tri

Theorem.

Arguments:

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

Hypotheses:

(blec)
(aleb)

Assertions:

(alec)

Proof:

Hyp Ref Line Expr
Hypo1(blec)
2(aleb)
2ax-tr3((blec)to(alec))
1, 3ax-mp4(alec)