<2tri

Theorem.

Arguments:

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

Hypotheses:

(deqb)
(ceqa)
(aeqb)

Assertions:

(ceqd)

Proof:

Hyp Ref Line Expr
Hypo1(deqb)
2(ceqa)
3(aeqb)
1ax-sym4(beqd)
2, 3, 42tri5(ceqd)