MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfan Unicode version

Theorem nfan 1842
Description: If  x is not free in  ph and  ps, it is not free in  ( ph  /\  ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.)
Hypotheses
Ref Expression
nfan.1  |-  F/ x ph
nfan.2  |-  F/ x ps
Assertion
Ref Expression
nfan  |-  F/ x
( ph  /\  ps )

Proof of Theorem nfan
StepHypRef Expression
1 nfan.1 . 2  |-  F/ x ph
2 nfan.2 . . 3  |-  F/ x ps
32a1i 11 . 2  |-  ( ph  ->  F/ x ps )
41, 3nfan1 1841 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:    /\ wa 359   F/wnf 1550
This theorem is referenced by:  nfnan  1843  nf3an  1845  hban  1846  nfbiOLD  1853  spimtOLD  1954  nfeqf  2014  dvelimh  2015  nfald2  2029  dvelimf  2050  cbval2  2054  cbvex2  2055  nfsb4t  2129  dvelimdf  2131  sbcom  2138  nfeud2  2266  mopick  2316  eupicka  2318  mopick2  2321  2eu6  2339  axbnd  2384  clelab  2524  nfel  2548  nfabd2  2558  2ralbida  2705  ralcom2  2832  reean  2834  cbvreu  2890  cbvrab  2914  ceqsex2  2952  vtocl2gaf  2978  rspce  3007  eqvincf  3024  elrabf  3051  rexab2  3061  morex  3078  reu2  3082  sbc2iegf  3187  rmo2  3206  rmo3  3208  csbiebt  3247  csbie2t  3255  cbvreucsf  3273  cbvrabcsf  3274  nfop  3960  nfopd  3961  eluniab  3987  dfnfc2  3993  nfopab  4233  cbvopab  4236  cbvopab1  4238  cbvopab2  4239  cbvopab1s  4240  mpteq12f  4245  nfmpt  4257  cbvmpt  4259  axrep3  4283  axrep4  4284  axrep5  4285  nfpo  4468  nfso  4469  nffr  4516  nfwe  4518  reusv2lem2  4684  reusv2lem3  4685  reusv6OLD  4693  onminex  4746  peano5  4827  nfxp  4863  opeliunxp  4888  nfco  4997  elrnmpt1  5078  nfimad  5171  iota2  5403  nffun  5435  imadif  5487  nffn  5500  nff  5548  nff1  5596  nffo  5611  nff1o  5631  fun11iun  5654  nffvd  5696  fv3  5703  fmptco  5860  opabex3d  5948  opabex3  5949  nfiso  6003  nfoprab  6085  mpt2eq123  6092  nfmpt2  6101  cbvoprab1  6103  cbvoprab2  6104  cbvoprab12  6105  cbvoprab3  6107  cbvmpt2x  6109  ovmpt2dxf  6158  dfoprab4f  6364  fmpt2x  6376  nfriotad  6517  cbvriota  6519  riota2df  6529  riota5f  6533  riotasv2d  6553  riotasv2dOLD  6554  riotasv2s  6555  nfrecs  6594  tfr3  6619  tz7.49  6661  erovlem  6959  nfixp  7040  nfixp1  7041  xpf1o  7228  nneneq  7249  ac6sfi  7310  nfoi  7439  wdom2d  7504  infpssrlem4  8142  hsmexlem2  8263  hsmexlem4  8265  domtriomlem  8278  axdc3lem2  8287  axdc4lem  8291  zorn2lem4  8335  zorn2lem5  8336  konigthlem  8399  axextnd  8422  axrepndlem2  8424  axrepnd  8425  axunnd  8427  axpowndlem2  8429  axpowndlem4  8431  axpownd  8432  axregndlem2  8434  axregnd  8435  axinfndlem1  8436  axinfnd  8437  zfcndrep  8445  zfcndinf  8449  nfsum1  12439  nfsum  12440  fsum2dlem  12509  fsum00  12532  mreexexd  13828  acsmapd  14559  gsum2d2lem  15502  dprd2d2  15557  neiptopnei  17151  neiptopreu  17152  neitr  17198  iunconlem  17443  iuncon  17444  ptcnplem  17606  ptcnp  17607  xkocnv  17799  isfildlem  17842  utopsnneiplem  18230  isucn2  18262  cfilucfilOLD  18552  cfilucfil  18553  restmetu  18570  ovolfiniun  19350  ovoliunlem3  19353  ovoliunnul  19356  volfiniun  19394  itg2splitlem  19593  itg2split  19594  isibl2  19611  nfitg  19619  cbvitg  19620  limciun  19734  chirred  23851  mo5f  23925  rmo3f  23935  rmo4fOLD  23936  cbvdisjf  23968  disjabrex  23977  disjabrexf  23978  funimass4f  23997  cbvmptf  24021  fmptcof2  24029  fcomptf  24030  funcnv4mpt  24038  xrofsup  24079  esumcl  24380  gsumesum  24404  esumlub  24405  esumcst  24408  esumfzf  24412  esumfsup  24413  hasheuni  24428  esumcvg  24429  measvunilem  24519  measvunilem0  24520  measvuni  24521  measinblem  24527  voliune  24538  volfiniune  24539  volmeas  24540  dstrvprob  24682  cvmcov  24903  iota5f  25135  dedekind  25140  dedekindle  25141  nfcprod1  25189  nfcprod  25190  fprod2dlem  25257  axextdist  25370  axext4dist  25371  trpredmintr  25448  wfrlem4  25473  frrlem4  25498  finminlem  26211  indexdom  26326  filbcmb  26332  sdclem2  26336  sdclem1  26337  fdc1  26340  mzpsubmpt  26690  mzpexpmpt  26692  eq0rabdioph  26725  eqrabdioph  26726  setindtr  26985  elunif  27554  rspcegf  27561  fnchoice  27567  refsumcn  27568  rfcnnnub  27574  fmul01  27577  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  infrglb  27589  climmulf  27597  climexp  27598  climsuse  27601  climrecf  27602  climinff  27604  stoweidlem3  27619  stoweidlem26  27642  stoweidlem27  27643  stoweidlem29  27645  stoweidlem31  27647  stoweidlem34  27650  stoweidlem35  27651  stoweidlem36  27652  stoweidlem39  27655  stoweidlem42  27658  stoweidlem43  27659  stoweidlem44  27660  stoweidlem46  27662  stoweidlem48  27664  stoweidlem49  27665  stoweidlem51  27667  stoweidlem52  27668  stoweidlem53  27669  stoweidlem54  27670  stoweidlem55  27671  stoweidlem56  27672  stoweidlem57  27673  stoweidlem58  27674  stoweidlem59  27675  stoweidlem60  27676  stoweidlem61  27677  stoweidlem62  27678  stoweid  27679  wallispilem3  27683  stirlinglem13  27702  stirling  27705  nfdfat  27861  bnj919  28842  bnj1146  28868  bnj1379  28908  bnj849  29002  bnj916  29010  bnj964  29020  bnj1014  29037  bnj1123  29061  bnj1228  29086  bnj1307  29098  bnj1321  29102  bnj1398  29109  bnj1408  29111  bnj1444  29118  bnj1445  29119  bnj1446  29120  bnj1449  29123  bnj1467  29129  bnj1463  29130  bnj1489  29131  bnj1491  29132  bnj1312  29133  bnj1525  29144  nfeqfNEW7  29192  spimtNEW7  29213  nfsb4twAUX7  29280  sbcomwAUX7  29291  nfald2OLD7  29401  dvelimfOLD7  29411  cbval2OLD7  29414  cbvex2OLD7  29415  nfsb4tOLD7  29429  nfsb4tw2AUXOLD7  29430  dvelimdfOLD7  29435  sbcomOLD7  29439  glbconxN  29860  pmapglb2xN  30254  cdlemefs32sn1aw  30896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator