ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfal Structured version   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  9321  bdsepnfALT  9323  setindft  9395  strcollnft  9414  strcollnfALT  9416
  Copyright terms: Public domain W3C validator