fv-negd

Theorem.

Arguments:

x (sv), phi (pr), psi (pr),

Hypotheses:

(phito(psitoforallxpsi))
(x bound in phi)

Assertions:

(phito(lnotpsitoforallxlnotpsi))

Proof:

Hyp Ref Line Expr
Hypo1(phito(psitoforallxpsi))
2(x bound in phi)
1, 2imgen>i3(phitoforallx(psitoforallxpsi))
fv-negt4(forallx(psitoforallxpsi)to(lnotpsitoforallxlnotpsi))
3, 4syl5(phito(lnotpsitoforallxlnotpsi))