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

Theorem nfal 1540
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 1484 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 1438 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nfi 1423 1 𝑥𝑦𝜑
Colors of variables: wff set class
Syntax hints:  wal 1314  wnf 1421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-7 1409  ax-gen 1410  ax-4 1472
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  nfnf  1541  nfa2  1543  aaan  1551  cbv3  1705  cbv2  1710  nfald  1718  cbval2  1873  nfsb4t  1967  nfeuv  1995  mo23  2018  bm1.1  2102  nfnfc1  2261  nfnfc  2265  nfeq  2266  sbcnestgf  3021  dfnfc2  3724  nfdisjv  3888  nfdisj1  3889  nffr  4241  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  exmidunben  11866  bdsepnft  13012  bdsepnfALT  13014  setindft  13090  strcollnft  13109  strcollnfALT  13111
  Copyright terms: Public domain W3C validator