tr-an

Theorem.

Arguments:

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

Assertions:

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

Proof:

Hyp Ref Line Expr
ax-tr1((aeqb)to((beqc)to(aeqc)))
1imp2(((aeqb)wedge(beqc))to(aeqc))