im.bldan<>d
Theorem.
Arguments:
(pr),
(pr),
(pr),
(pr),
(pr),
Hypotheses:
(
(
))
(
(
))
Assertions:
(
((
)
(
)))
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
(
))
2
(
(
))
praeclarum
3
(((
)
(
))
((
)
(
)))
1, 2
jca
4
(
((
)
(
)))
3, 4
syl
5
(
((
)
(
)))