pm3.2im

Theorem.

Arguments:

phi (pr), psi (pr),

Assertions:

(phito(psitolnot(phitolnotpsi)))

Proof:

Hyp Ref Line Expr
mpclosed1(phito((phitolnotpsi)tolnotpsi))
1con>2(phito(psitolnot(phitolnotpsi)))