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

Theorem nfal 1556
 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 1500 . . 3 (𝜑 → ∀𝑥𝜑)
32hbal 1454 . 2 (∀𝑦𝜑 → ∀𝑥𝑦𝜑)
43nfi 1439 1 𝑥𝑦𝜑
 Colors of variables: wff set class Syntax hints:  ∀wal 1330  Ⅎwnf 1437 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 1424  ax-7 1425  ax-gen 1426  ax-4 1488 This theorem depends on definitions:  df-bi 116  df-nf 1438 This theorem is referenced by:  nfnf  1557  nfa2  1559  aaan  1567  cbv3  1721  cbv2  1726  nfald  1734  cbval2  1894  nfsb4t  1990  nfeuv  2018  mo23  2041  bm1.1  2125  nfnfc1  2285  nfnfc  2289  nfeq  2290  sbcnestgf  3057  dfnfc2  3763  nfdisjv  3927  nfdisj1  3928  nffr  4280  exmidfodomrlemr  7078  exmidfodomrlemrALT  7079  exmidunben  11995  bdsepnft  13276  bdsepnfALT  13278  setindft  13354  strcollnft  13373  pw1nct  13390
 Copyright terms: Public domain W3C validator