<2tri-r

Theorem.

Arguments:

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

Hypotheses:

(deqb)
(ceqa)
(aeqb)

Assertions:

(deqc)

Proof:

Hyp Ref Line Expr
Hypo1(deqb)
2(ceqa)
3(aeqb)
1, 2, 3<2tri4(ceqd)
4ax-sym5(deqc)