ancomsd
Theorem.
Arguments:
(pr),
(pr),
(pr),
(pr),
Hypotheses:
(
((
)
))
Assertions:
(
((
)
))
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
((
)
))
ancom
2
((
)
(
))
1, 2
brpi32
3
(
((
)
))