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

Theorem nfal 1465
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 xyφ

Proof of Theorem nfal
StepHypRef Expression
1 nfal.1 . . . 4 xφ
21nfri 1409 . . 3 (φxφ)
32hbal 1363 . 2 (yφxyφ)
43nfi 1348 1 xyφ
Colors of variables: wff set class
Syntax hints:  wal 1240  wnf 1346
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-4 1397
This theorem depends on definitions:  df-bi 110  df-nf 1347
This theorem is referenced by:  nfnf  1466  nfa2  1468  aaan  1476  cbv3  1627  cbv2  1632  nfald  1640  cbval2  1793  nfsb4t  1887  nfeuv  1915  mo23  1938  bm1.1  2022  nfnfc1  2178  nfnfc  2181  nfeq  2182  sbcnestgf  2891  dfnfc2  3589  nfdisjv  3748  nfdisj1  3749  bdsepnft  9342  bdsepnfALT  9344  setindft  9425  strcollnft  9444  strcollnfALT  9446
  Copyright terms: Public domain W3C validator