eqt<>d2

Theorem.

Arguments:

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

Hypotheses:

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

Assertions:

((phiwedgepsi)to((aeqc)leftrightarrow(beqd)))

Proof:

Hyp Ref Line Expr
Hypo1(psito(ceqd))
2(phito(aeqb))
2siman<3((phiwedgepsi)to(aeqb))
1siman>4((phiwedgepsi)to(ceqd))
3, 4eqt<>d5((phiwedgepsi)to((aeqc)leftrightarrow(beqd)))