neqcom

Theorem.

Arguments:

a (obj), b (obj),

Assertions:

((aneb)leftrightarrow(bnea))

Proof:

Hyp Ref Line Expr
com1((aeqb)leftrightarrow(beqa))
1eqneqi2((aneb)leftrightarrow(bnea))