>2tri-r

Theorem.

Arguments:

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

Hypotheses:

(beqd)
(aeqc)
(aeqb)

Assertions:

(deqc)

Proof:

Hyp Ref Line Expr
Hypo1(beqd)
2(aeqc)
3(aeqb)
1, 2, 3>2tri4(ceqd)
4ax-sym5(deqc)