rp-2>
Theorem.
Arguments:
(st),
(coll),
(coll),
Hypotheses:
(
)
(
)
Assertions:
(
)
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
)
2
(
)
1
eqt>
3
((
)
(
))
2, 3
ax-mp
4
(
)