eqt<>pd

Theorem.

Arguments:

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

Hypotheses:

(phito(ceqd))
(phito(aeqb))

Assertions:

(phito((altc)leftrightarrow(bltd)))

Proof:

Hyp Ref Line Expr
Hypo1(phito(ceqd))
2(phito(aeqb))
2eqt<p3(phito((altd)leftrightarrow(bltd)))
1eqt>p4(phito((altc)leftrightarrow(altd)))
3, 4bitrd5(phito((altc)leftrightarrow(bltd)))