tr-an<

Theorem.

Arguments:

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

Assertions:

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

Proof:

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