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

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

Proof of Theorem nfal
StepHypRef Expression
1 nfal.1 . . . 4
21nfri 1453 . . 3
32hbal 1407 . 2
43nfi 1392 1
 Colors of variables: wff set class Syntax hints:  wal 1283  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