eqt<n
Theorem.
Arguments:
(obj),
(obj),
(obj),
Assertions:
((
)
((
)
(
)))
Proof:
Hyp
Ref
Line
Expr
eqt<
1
((
)
((
)
(
)))
1
bi.bldnegd
2
((
)
(
(
)
(
)))
df-neq
3
((
)
(
))
df-neq
4
((
)
(
))
2, 3, 4
<2bitrg
5
((
)
((
)
(
)))