Theorem nfn 1793

Description: If x is not free in φ, it is not free in ¬ φ. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfn.1	⊢ Ⅎxφ

Assertion

Ref	Expression
nfn	⊢ Ⅎx ¬ φ

Proof of Theorem nfn

Step	Hyp	Ref	Expression
1		nfn.1	. . . 4 ⊢ Ⅎxφ
2	1	a1i 10	. . 3 ⊢ ( ⊤ → Ⅎxφ)
3	2	nfnd 1791	. 2 ⊢ ( ⊤ → Ⅎx ¬ φ)
4	3	trud 1323	1 ⊢ Ⅎx ¬ φ

Syntax hints:  ¬ wn 3   ⊤ wtru 1316  Ⅎwnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by:  nfnan  1825  nfanOLD  1826  nfor  1836  nfexOLD  1844  19.32  1875  nfnae  1956  equsex  1962  spime  1976  cbvex  1985  ax15  2021  sb8e  2093  mo  2226  euor  2231  euor2  2272  2mo  2282  nfne  2611  nfnel  2612  nfrex  2670  cbvrexf  2831  spcimegf  2934  spcegf  2936  cbvrexcsf  3200  rexxpf  4829