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

Theorem nfal 1538
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 1482 . . 3  |-  ( ph  ->  A. x ph )
32hbal 1436 . 2  |-  ( A. y ph  ->  A. x A. y ph )
43nfi 1421 1  |-  F/ x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1312   F/wnf 1419
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 1406  ax-7 1407  ax-gen 1408  ax-4 1470
This theorem depends on definitions:  df-bi 116  df-nf 1420
This theorem is referenced by:  nfnf  1539  nfa2  1541  aaan  1549  cbv3  1703  cbv2  1708  nfald  1716  cbval2  1871  nfsb4t  1965  nfeuv  1993  mo23  2016  bm1.1  2100  nfnfc1  2259  nfnfc  2263  nfeq  2264  sbcnestgf  3019  dfnfc2  3722  nfdisjv  3886  nfdisj1  3887  nffr  4239  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  exmidunben  11834  bdsepnft  12896  bdsepnfALT  12898  setindft  12974  strcollnft  12993  strcollnfALT  12995
  Copyright terms: Public domain W3C validator