rp-1<d

Theorem.

Arguments:

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

Hypotheses:

(phito(ceqa))
(phito(ainb))

Assertions:

(phito(cinb))

Proof:

Hyp Ref Line Expr
Hypo1(phito(ceqa))
2(phito(ainb))
2eqt<a3(phito((ceqa)to(cinb)))
1, 3mpd4(phito(cinb))