fv-neg

Theorem.

Arguments:

x (sv), phi (pr),

Hypotheses:

(phitoforallxphi)

Assertions:

(lnotphitoforallxlnotphi)

Proof:

Hyp Ref Line Expr
Hypo1(phitoforallxphi)
1con2(lnotforallxphitolnotphi)
2im.bldal3(forallxlnotforallxphitoforallxlnotphi)
ax64(lnotforallxlnotforallxphitophi)
4con<5(lnotphitoforallxlnotforallxphi)
3, 5syl6(lnotphitoforallxlnotphi)