ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfal GIF version

Theorem nfal 1523
Description: If 𝑥 is not free in 𝜑, it is not free in 𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfal.1 𝑥𝜑
Assertion
Ref Expression
nfal 𝑥𝑦𝜑

Proof of Theorem nfal
StepHypRef Expression
1 nfal.1 . . . 4 𝑥𝜑
21nfri 1467 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 1421 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nfi 1406 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wal 1297  wnf 1404
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-4 1455
This theorem depends on definitions:  df-bi 116  df-nf 1405
This theorem is referenced by:  nfnf  1524  nfa2  1526  aaan  1534  cbv3  1688  cbv2  1693  nfald  1701  cbval2  1856  nfsb4t  1950  nfeuv  1978  mo23  2001  bm1.1  2085  nfnfc1  2243  nfnfc  2247  nfeq  2248  sbcnestgf  3001  dfnfc2  3701  nfdisjv  3864  nfdisj1  3865  nffr  4209  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  exmidunben  11731  bdsepnft  12666  bdsepnfALT  12668  setindft  12748  strcollnft  12767  strcollnfALT  12769
  Copyright terms: Public domain W3C validator