rp-2>d

Theorem.

Arguments:

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

Hypotheses:

(phito(bequivc))
(phito(ainb))

Assertions:

(phito(ainc))

Proof:

Hyp Ref Line Expr
Hypo1(phito(bequivc))
2(phito(ainb))
1eqt>3(phito((ainb)leftrightarrow(ainc)))
3bi>4(phito((ainb)to(ainc)))
2, 4mpd5(phito(ainc))