>2trd

Theorem.

Arguments:

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

Hypotheses:

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

Assertions:

(phito(cled))

Proof:

Hyp Ref Line Expr
Hypo1(phito(beqd))
2(phito(aeqc))
3(phito(aleb))
1, 2eqt<>d4(phito((aleb)leftrightarrow(cled)))
4bi>5(phito((aleb)to(cled)))
3, 5mpd6(phito(cled))