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

Theorem nfal 1509
Description: If  x is not free in  ph, it is not free in  A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfal.1  |-  F/ x ph
Assertion
Ref Expression
nfal  |-  F/ x A. y ph

Proof of Theorem nfal
StepHypRef Expression
1 nfal.1 . . . 4  |-  F/ x ph
21nfri 1453 . . 3  |-  ( ph  ->  A. x ph )
32hbal 1407 . 2  |-  ( A. y ph  ->  A. x A. y ph )
43nfi 1392 1  |-  F/ x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1283   F/wnf 1390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-4 1441
This theorem depends on definitions:  df-bi 115  df-nf 1391
This theorem is referenced by:  nfnf  1510  nfa2  1512  aaan  1520  cbv3  1671  cbv2  1676  nfald  1684  cbval2  1838  nfsb4t  1932  nfeuv  1960  mo23  1983  bm1.1  2067  nfnfc1  2223  nfnfc  2226  nfeq  2227  sbcnestgf  2954  dfnfc2  3627  nfdisjv  3786  nfdisj1  3787  nffr  4112  bdsepnft  10836  bdsepnfALT  10838  setindft  10918  strcollnft  10937  strcollnfALT  10939
  Copyright terms: Public domain W3C validator