tri>

Theorem.

Arguments:

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

Hypotheses:

(aeqc)
(aeqb)

Assertions:

(beqc)

Proof:

Hyp Ref Line Expr
Hypo1(aeqc)
2(aeqb)
2ax-sym3(beqa)
1, 3tri4(beqc)