rp-1>d

Theorem.

Arguments:

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

Hypotheses:

(phito(aeqc))
(phito(aleb))

Assertions:

(phito(cleb))

Proof:

Hyp Ref Line Expr
Hypo1(phito(aeqc))
2(phito(aleb))
1eqt<3(phito((aleb)leftrightarrow(cleb)))
3bi>4(phito((aleb)to(cleb)))
2, 4mpd5(phito(cleb))