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

Theorem nfal 1513
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 1457 . . 3  |-  ( ph  ->  A. x ph )
32hbal 1411 . 2  |-  ( A. y ph  ->  A. x A. y ph )
43nfi 1396 1  |-  F/ x A. y ph
Colors of variables: wff set class
Syntax hints:   A.wal 1287   F/wnf 1394
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 1381  ax-7 1382  ax-gen 1383  ax-4 1445
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  nfnf  1514  nfa2  1516  aaan  1524  cbv3  1677  cbv2  1682  nfald  1690  cbval2  1844  nfsb4t  1938  nfeuv  1966  mo23  1989  bm1.1  2073  nfnfc1  2231  nfnfc  2235  nfeq  2236  sbcnestgf  2977  dfnfc2  3666  nfdisjv  3826  nfdisj1  3827  nffr  4167  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  bdsepnft  11435  bdsepnfALT  11437  setindft  11517  strcollnft  11536  strcollnfALT  11538
  Copyright terms: Public domain W3C validator