tri-r

Theorem.

Arguments:

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

Hypotheses:

(beqc)
(aeqb)

Assertions:

(ceqa)

Proof:

Hyp Ref Line Expr
Hypo1(beqc)
2(aeqb)
1, 2tri3(aeqc)
3ax-sym4(ceqa)