neq>

Theorem.

Arguments:

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

Assertions:

(((cina)wedgelnot(cinb))tolnot(aequivb))

Proof:

Hyp Ref Line Expr
eqt>1((aequivb)to((cina)leftrightarrow(cinb)))
1bi>2((aequivb)to((cina)to(cinb)))
2com12i3((cina)to((aequivb)to(cinb)))
3con4((cina)to(lnot(cinb)tolnot(aequivb)))
4imp5(((cina)wedgelnot(cinb))tolnot(aequivb))