eqt>
Theorem.
Arguments:
(obj),
(obj),
(obj),
Assertions:
((
)
((
)
(
)))
Proof:
Hyp
Ref
Line
Expr
com
1
((
)
(
))
com
2
((
)
(
))
1, 2
bi.bldbi<>
3
(((
)
(
))
((
)
(
)))
eqt<
4
((
)
((
)
(
)))
3, 4
brpi22
5
((
)
((
)
(
)))