Theorem nfal 1842

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

Hypothesis

Ref	Expression
nfal.1	⊢ Ⅎxφ

Assertion

Ref	Expression
nfal	⊢ Ⅎx∀yφ

Proof of Theorem nfal

Step	Hyp	Ref	Expression
1		nfal.1	. . . 4 ⊢ Ⅎxφ
2	1	nfri 1762	. . 3 ⊢ (φ → ∀xφ)
3	2	hbal 1736	. 2 ⊢ (∀yφ → ∀x∀yφ)
4	3	nfi 1551	1 ⊢ Ⅎx∀yφ

Syntax hints:  ∀wal 1540  Ⅎ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-7 1734  ax-11 1746

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

This theorem is referenced by:  nfexOLD  1844  nfnf  1845  nfnfOLD  1846  nfald  1852  nfaldOLD  1853  nfa2  1855  aaan  1884  pm11.53  1893  19.12vv  1898  cbval2  2004  sb8  2092  euf  2210  mo  2226  2mo  2282  2eu3  2286  bm1.1  2338  nfnfc1  2493  nfnfc  2496  nfeq  2497  sbcnestgf  3184  dfnfc2  3910