msca

Theorem.

Arguments:

x (sv), y (st), phi (pr), phi (pr), psi (pr), chi (pr), theta (pr),

Distinct variable conditions:

(x, y),

Hypotheses:

(thetato(psitolnotchi))
(phito(psitochi))

Assertions:

(phito(psitolnottheta))

Proof:

Hyp Ref Line Expr
Hypo1(thetato(psitolnotchi))
2(phito(psitochi))
siman>3((phiwedgepsi)topsi)
2imp4((phiwedgepsi)tochi)
3, 4jc-pre5((phiwedgepsi)tolnot(psitolnotchi))
1con6(lnot(psitolnotchi)tolnottheta)
5, 6syl7((phiwedgepsi)tolnottheta)
7exp8(phito(psitolnottheta))