neq<

Theorem.

Arguments:

a (st), b (st), c (coll),

Assertions:

(((ainc)wedgelnot(binc))tolnot(aeqb))

Proof:

Hyp Ref Line Expr
eqt<1((aeqb)to((ainc)leftrightarrow(binc)))
1bi>2((aeqb)to((ainc)to(binc)))
2com12i3((ainc)to((aeqb)to(binc)))
3con4((ainc)to(lnot(binc)tolnot(aeqb)))
4imp5(((ainc)wedgelnot(binc))tolnot(aeqb))