tri

Theorem.

Arguments:

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

Hypotheses:

(beqc)
(aeqb)

Assertions:

(aeqc)

Proof:

Hyp Ref Line Expr
Hypo1(beqc)
2(aeqb)
2ax-tr3((beqc)to(aeqc))
1, 3ax-mp4(aeqc)