<2trd-r

Theorem.

Arguments:

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

Hypotheses:

(phito(deqb))
(phito(ceqa))
(phito(aeqb))

Assertions:

(phito(deqc))

Proof:

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