rp-2>d
Theorem.
Arguments:
(st),
(coll),
(coll),
(pr),
Hypotheses:
(
(
))
(
(
))
Assertions:
(
(
))
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
(
))
2
(
(
))
1
eqt>
3
(
((
)
(
)))
3
bi>
4
(
((
)
(
)))
2, 4
mpd
5
(
(
))