tr-an>

Theorem.

Arguments:

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

Assertions:

(((aeqb)wedge(aeqc))to(beqc))

Proof:

Hyp Ref Line Expr
eqt<1((aeqb)to((aeqc)leftrightarrow(beqc)))
1bi>2((aeqb)to((aeqc)to(beqc)))
2imp3(((aeqb)wedge(aeqc))to(beqc))