>2tri

Theorem.

Arguments:

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

Hypotheses:

(beqd)
(aeqc)
(aeqb)

Assertions:

(ceqd)

Proof:

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