eqt<a

Theorem.

Arguments:

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

Assertions:

((ainb)to((ceqa)to(cinb)))

Proof:

Hyp Ref Line Expr
eqt<1((ceqa)to((cinb)leftrightarrow(ainb)))
1bi<2((ceqa)to((ainb)to(cinb)))
2com12i3((ainb)to((ceqa)to(cinb)))