jc-pre

Theorem.

Arguments:

phi (pr), psi (pr), chi (pr),

Hypotheses:

(phitochi)
(phitopsi)

Assertions:

(phitolnot(psitolnotchi))

Proof:

Hyp Ref Line Expr
Hypo1(phitochi)
2(phitopsi)
pm3.2im3(psito(chitolnot(psitolnotchi)))
1, 2, 3sylc4(phitolnot(psitolnotchi))