eqt>n

Theorem.

Arguments:

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

Assertions:

((aeqb)to((cnea)leftrightarrow(cneb)))

Proof:

Hyp Ref Line Expr
eqt>1((aeqb)to((ceqa)leftrightarrow(ceqb)))
1bi.bldnegd2((aeqb)to(lnot(ceqa)leftrightarrowlnot(ceqb)))
df-neq3((cnea)leftrightarrowlnot(ceqa))
df-neq4((cneb)leftrightarrowlnot(ceqb))
2, 3, 4<2bitrg5((aeqb)to((cnea)leftrightarrow(cneb)))