eqt<n

Theorem.

Arguments:

a (obj), b (obj), c (obj),

Assertions:

((aeqb)to((anec)leftrightarrow(bnec)))

Proof:

Hyp Ref Line Expr
eqt<1((aeqb)to((aeqc)leftrightarrow(beqc)))
1bi.bldnegd2((aeqb)to(lnot(aeqc)leftrightarrowlnot(beqc)))
df-neq3((anec)leftrightarrowlnot(aeqc))
df-neq4((bnec)leftrightarrowlnot(beqc))
2, 3, 4<2bitrg5((aeqb)to((anec)leftrightarrow(bnec)))