rp-2<g

Theorem.

Arguments:

a (st), b (coll), c (coll), phi (pr),

Hypotheses:

(cequivb)
(phito(ainb))

Assertions:

(phito(ainc))

Proof:

Hyp Ref Line Expr
Hypo1(cequivb)
2(phito(ainb))
1ax13(phito(cequivb))
2, 3rp-2<d4(phito(ainc))