<imtrd
Theorem.
Arguments:
(pr),
(pr),
(pr),
(pr),
(pr),
Hypotheses:
(
(
))
(
(
))
(
(
))
Assertions:
(
(
))
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
(
))
2
(
(
))
3
(
(
))
2
bicom
4
(
(
))
1
bicom
5
(
(
))
3, 4, 5
>imtrd
6
(
(
))