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

Theorem nfan 1613
Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
Hypotheses
Ref Expression
nfan.1 𝑥𝜑
nfan.2 𝑥𝜓
Assertion
Ref Expression
nfan 𝑥(𝜑𝜓)

Proof of Theorem nfan
StepHypRef Expression
1 nfan.1 . 2 𝑥𝜑
2 nfan.2 . . 3 𝑥𝜓
32a1i 9 . 2 (𝜑 → Ⅎ𝑥𝜓)
41, 3nfan1 1612 1 𝑥(𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wa 104  wnf 1508
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558
This theorem depends on definitions:  df-bi 117  df-nf 1509
This theorem is referenced by:  nf3an  1614  cbvex2  1971  nfsbxyt  1996  nfsbv  2000  sbcomxyyz  2025  nfsb4t  2067  clelab  2357  nfel  2383  2ralbida  2553  r19.29an  2675  reean  2702  nfrabw  2714  cbvrmow  2716  cbvrexfw  2757  cbvrexf  2759  cbvreu  2765  cbvrab  2800  ceqsex2  2844  vtocl2gaf  2871  rspce  2905  eqvincf  2931  elrabf  2960  elrab3t  2961  rexab2  2972  morex  2990  reu2  2994  rmo3f  3003  sbc2iegf  3102  reu8nf  3113  rmo2ilem  3122  rmo3  3124  csbiebt  3167  csbie2t  3176  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  rabsnifsb  3737  nfopd  3879  eluniab  3905  dfnfc2  3911  nfdisjv  4076  disjiun  4083  nfopab  4157  cbvopab  4160  cbvopab1  4162  cbvopab2  4163  cbvopab1s  4164  mpteq12f  4169  nfmpt  4181  cbvmptf  4183  cbvmpt  4184  repizf2  4252  nfpo  4398  nfso  4399  nfwe  4452  onintonm  4615  peano2  4693  nfxp  4752  opeliunxp  4781  nfco  4895  elrnmpt1  4983  nfimad  5085  iota2  5316  dffun4f  5342  nffun  5349  imadif  5410  funimaexglem  5413  nffn  5426  nff  5479  nff1  5540  nffo  5558  nff1o  5581  fun11iun  5604  nffvd  5651  fv3  5662  fmptco  5813  nfiso  5947  cbvriota  5983  riota2df  5993  riota5f  5998  nfoprab  6073  mpoeq123  6080  nfmpo  6090  cbvoprab1  6093  cbvoprab2  6094  cbvoprab12  6095  cbvoprab3  6097  cbvmpox  6099  ovmpodxf  6147  elovmporab  6222  elovmporab1w  6223  opabex3d  6283  opabex3  6284  uchoice  6300  dfoprab4f  6356  fmpox  6365  spc2ed  6398  cnvoprab  6399  f1od2  6400  opeliunxp2f  6404  nfrecs  6473  tfri3  6533  nffrec  6562  erovlem  6796  nfixpxy  6886  nfixp1  6887  modom  6994  xpf1o  7030  nneneq  7043  ac6sfi  7087  opabfi  7132  nfsup  7191  exmidomni  7341  fodjuomnilemdc  7343  ismkvnex  7354  mkvprop  7357  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  cc3  7487  caucvgsrlemgt1  8015  suplocsrlem  8028  axpre-suploclemres  8121  supinfneg  9829  infsupneg  9830  zsupcllemstep  10490  nninfinf  10706  reuccatpfxs1  11329  fimaxre2  11789  nfsum1  11918  nfsum  11919  fsumsplitf  11971  fsum2dlemstep  11997  fsum00  12025  nfcprod1  12117  nfcprod  12118  prodeq2  12120  fprod2dlemstep  12185  fprodsplitf  12195  fprodsplit1f  12197  fprodap0f  12199  fprodle  12203  bezoutlemmain  12571  bezoutlemzz  12575  bezout  12584  exmidunben  13049  ctiunctlemfo  13062  ctiunct  13063  mulcncf  15335  ellimc3apf  15387  limccnp2cntop  15404  bdsepnft  16503  bdsepnfALT  16505  bj-findis  16595  strcollnft  16600  strcollnfALT  16602  pw1nct  16625  isomninnlem  16655  trirec0  16669  iswomninnlem  16674  ismkvnnlem  16677
  Copyright terms: Public domain W3C validator