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

Theorem nfan 2010
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 2009 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 371   F/wnf 1666
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-12 1932
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-nf 1667
This theorem is referenced by:  nfnan  2011  nf3an  2012  hban  2013  nfeqf  2138  nfald2  2164  nfsb4t  2217  2ax6elem  2277  eupicka  2365  mopick2  2368  2mo  2379  axbnd  2429  clelab  2575  nfabd2  2610  2ralbida  2828  r19.29an  2930  ralcom2  2954  reean  2956  cbvreu  3016  cbvrab  3042  ceqsex2  3085  vtocl2gaf  3113  rspce  3144  eqvincf  3166  elrabf  3193  elrab3t  3194  rexab2  3204  morex  3221  reu2  3225  reu2eqd  3234  sbc2iegf  3333  rmo2  3355  rmo3  3357  csbiebt  3382  csbie2t  3391  cbvreucsf  3396  cbvrabcsf  3397  rabsnifsb  4039  nfop  4181  nfopd  4182  eluniab  4208  dfnfc2  4215  rabasiun  4281  nfopab  4467  cbvopab  4470  cbvopab1  4472  cbvopab2  4473  cbvopab1s  4474  mpteq12f  4478  nfmpt  4490  cbvmptf  4492  cbvmpt  4493  axrep3  4517  axrep4  4518  axrep5  4519  reusv2lem2  4604  reusv2lem3  4605  nfpo  4759  nfso  4760  nffr  4807  nfwe  4809  nfxp  4860  opeliunxp  4885  nfco  4999  elrnmpt1  5082  nfimad  5176  elsnxp  5377  iota2  5571  nffun  5603  imadif  5656  nffn  5670  nff  5722  nff1  5775  nffo  5790  nff1o  5810  nffvd  5872  fv3  5876  fmptco  6054  fsnex  6179  nfiso  6213  nfriotad  6258  cbvriota  6260  riota2df  6270  riota5f  6274  oprabv  6336  nfoprab  6340  mpt2eq123  6347  nfmpt2  6357  cbvoprab1  6360  cbvoprab2  6361  cbvoprab12  6362  cbvoprab3  6364  cbvmpt2x  6366  ovmpt2dxf  6419  elovmpt2rab  6512  elovmpt2rab1  6513  onminex  6631  peano5  6713  fun11iun  6750  opabex3d  6768  opabex3  6769  dfoprab4f  6848  fmpt2x  6856  opeliunxp2f  6953  nfwrecs  7027  wfrlem4  7036  tfr3  7114  tz7.49  7159  erovlem  7456  nfixp  7538  nfixp1  7539  xpf1o  7731  nneneq  7752  ac6sfi  7812  nfoi  8026  wdom2d  8092  infpssrlem4  8733  hsmexlem2  8854  hsmexlem4  8856  domtriomlem  8869  axdc3lem2  8878  axdc4lem  8882  zorn2lem4  8926  zorn2lem5  8927  konigthlem  8990  axextnd  9013  axrepndlem2  9015  axrepnd  9016  axunnd  9018  axpowndlem2  9020  axpowndlem4  9022  axpownd  9023  axregndlem2  9025  axregnd  9026  axinfndlem1  9027  axinfnd  9028  zfcndrep  9036  zfcndinf  9040  dedekind  9794  dedekindle  9795  fsuppmapnn0fiublem  12199  fsuppmapnn0fiub  12200  fsuppmapnn0fiubex  12201  nfsum1  13749  nfsum  13750  fsum2dlem  13824  fsum00  13851  nfcprod1  13957  nfcprod  13958  fprod2dlem  14027  fprodsplitf  14035  fprodsplit1f  14037  fprodle  14043  lcmfunsnlem1  14603  lcmfunsnlem2lem1  14604  lcmfunsnlem2  14606  mreexexd  15547  acsmapd  16417  gsum2d2lem  17598  dprd2d2  17670  gsummoncoe1  18891  gsummatr01lem4  19676  cpmatmcllem  19735  pmatcollpwfi  19799  cayleyhamilton1  19909  neiptopnei  20141  neiptopreu  20142  neitr  20189  iunconlem  20435  iuncon  20436  ptcnplem  20629  ptcnp  20630  xkocnv  20822  isfildlem  20865  utopsnneiplem  21255  isucn2  21287  cfilucfil  21567  restmetu  21578  ovolfiniun  22447  ovoliunlem3  22450  ovoliunnul  22453  volfiniun  22493  itg2splitlem  22699  itg2split  22700  isibl2  22717  nfitg  22725  cbvitg  22726  limciun  22842  istrkg2ld  24501  chirred  28041  spc2ed  28099  mo5f  28113  rmo3f  28124  rmo4fOLD  28125  foresf1o  28132  cbvdisjf  28175  disjabrex  28185  disjabrexf  28186  funimass4f  28227  fmptcof2  28252  fcomptf  28253  acunirnmpt2  28255  acunirnmpt2f  28256  aciunf1lem  28257  funcnv4mpt  28266  cnvoprab  28301  f1od2  28302  fpwrelmap  28311  xrofsup  28346  nn0min  28377  2sqmo  28403  isarchiofld  28573  reff  28659  locfinreflem  28660  cmpcref  28670  ordtconlem1  28723  esumcl  28844  gsumesum  28873  esumlub  28874  esumcst  28877  esumrnmpt2  28882  esumfzf  28883  esumfsup  28884  hasheuni  28899  esumcvg  28900  esumgect  28904  esumcvgre  28905  esum2dlem  28906  esum2d  28907  esumiun  28908  ldsysgenld  28975  sigapildsyslem  28976  sigapildsys  28977  ldgenpisyslem1  28978  measvunilem  29027  measvunilem0  29028  measvuni  29029  measinblem  29035  voliune  29045  volfiniune  29046  volmeas  29047  oms0  29118  omssubadd  29121  oms0OLD  29122  omssubaddOLD  29125  eulerpartlemgvv  29202  dstrvprob  29297  bnj919  29571  bnj1146  29596  bnj1379  29635  bnj849  29729  bnj916  29737  bnj964  29747  bnj1014  29764  bnj1123  29788  bnj1228  29813  bnj1307  29825  bnj1321  29829  bnj1398  29836  bnj1408  29838  bnj1444  29845  bnj1445  29846  bnj1446  29847  bnj1449  29850  bnj1467  29856  bnj1463  29857  bnj1489  29858  bnj1491  29859  bnj1312  29860  bnj1525  29871  cvmcov  29979  iota5f  30350  axextdist  30439  axext4dist  30440  trpredmintr  30465  nfwlim  30498  frrlem4  30510  finminlem  30967  bj-axrep3  31398  bj-axrep4  31399  bj-axrep5  31400  isbasisrelowllem1  31751  isbasisrelowllem2  31752  wl-cbvalnaed  31858  wl-2sb6d  31881  wl-sbalnae  31885  wl-mo2tf  31893  wl-eutf  31895  wl-ax11-lem3  31910  phpreu  31922  poimirlem26  31959  poimirlem27  31960  heicant  31968  mbfposadd  31981  ftc1anclem5  32014  indexdom  32054  filbcmb  32060  sdclem2  32064  sdclem1  32065  fdc1  32068  riotasv2d  32523  riotasv2s  32524  glbconxN  32937  pmapglb2xN  33331  cdlemefs32sn1aw  33975  mzpsubmpt  35579  mzpexpmpt  35581  eq0rabdioph  35613  eqrabdioph  35614  setindtr  35873  ss2iundf  36245  binomcxplemnotnn0  36699  iunconlem2  37326  elunif  37331  rspcegf  37338  fnchoice  37344  refsumcn  37345  rfcnnnub  37351  uzwo4  37386  fiiuncl  37400  rspcef  37410  disjf1  37451  wessf1ornlem  37453  disjrnmpt2  37457  disjf1o  37460  fompt  37461  disjinfi  37462  choicefi  37475  upbdrech  37517  ssfiunibd  37521  supxrgere  37550  supxrgelem  37554  supxrge  37555  xralrple2  37571  iccshift  37613  iooshift  37617  fsumclf  37639  fsumsplitf  37640  fsummulc1f  37641  fsumsplit1  37645  fsumf1of  37647  fsumreclf  37649  fsumlessf  37650  fmul01  37652  fmuldfeqlem1  37654  fmuldfeq  37655  fmul01lt1lem1  37656  fmul01lt1lem2  37657  infrglbOLD  37663  fprodexp  37668  mccl  37672  climmulf  37676  climexp  37677  climsuse  37681  climrecf  37682  climinff  37684  climinffOLD  37685  climaddf  37689  mullimc  37690  islptre  37693  climf  37696  mullimcf  37697  rexlim2d  37699  idlimc  37700  limcperiod  37702  limcrecl  37703  islpcn  37713  limsupre  37715  limsupreOLD  37716  limcleqr  37719  addlimc  37723  limclner  37726  cncficcgt0  37760  cncfioobd  37769  dvmptmulf  37806  dvnmul  37812  dvmptfprodlem  37813  dvmptfprod  37814  dvnprodlem1  37815  dvnprodlem2  37816  iblsplitf  37841  itgperiod  37852  stoweidlem3  37857  stoweidlem26  37880  stoweidlem27  37881  stoweidlem29  37883  stoweidlem29OLD  37884  stoweidlem31  37886  stoweidlem34  37889  stoweidlem35  37890  stoweidlem36  37891  stoweidlem39  37894  stoweidlem42  37897  stoweidlem43  37898  stoweidlem44  37899  stoweidlem46  37901  stoweidlem48  37903  stoweidlem49  37904  stoweidlem51  37906  stoweidlem52  37907  stoweidlem53  37908  stoweidlem54  37909  stoweidlem55  37910  stoweidlem56  37911  stoweidlem57  37912  stoweidlem58  37913  stoweidlem59  37914  stoweidlem60  37915  stoweidlem61  37916  stoweidlem62  37917  stoweidlem62OLD  37918  stoweid  37919  wallispilem3  37923  stirlinglem13  37942  stirling  37945  fourierdlem16  37979  fourierdlem21  37984  fourierdlem22  37985  fourierdlem31  37994  fourierdlem31OLD  37995  fourierdlem39  38003  fourierdlem48  38012  fourierdlem51  38015  fourierdlem53  38017  fourierdlem68  38032  fourierdlem71  38035  fourierdlem73  38037  fourierdlem80  38044  fourierdlem81  38045  fourierdlem86  38050  fourierdlem87  38051  fourierdlem93  38057  fourierdlem94  38058  fourierdlem103  38067  fourierdlem104  38068  fourierdlem112  38076  fourierdlem113  38077  elaa2  38093  etransclem32  38125  salexct  38187  sge0revalmpt  38214  sge0f1o  38218  sge0lefi  38234  sge0resplit  38242  sge0lempt  38246  sge0iunmptlemre  38251  sge0fodjrnlem  38252  sge0iunmpt  38254  sge0ltfirpmpt2  38262  sge0isum  38263  sge0xp  38265  sge0isummpt2  38268  sge0xadd  38271  sge0pnffsumgt  38278  sge0gtfsumgt  38279  sge0uzfsumgt  38280  iundjiun  38292  meadjiun  38298  ismeannd  38299  caragenfiiuncl  38330  omeiunltfirp  38334  ovnsubaddlem2  38387  hoidmvval0  38403  hoidmvlelem1  38411  hoidmvlelem3  38413  hoidmvlelem5  38415  ovnlecvr2  38426  hspdifhsp  38432  hoiqssbllem2  38439  hoiqssbllem3  38440  hspmbllem2  38443  opnvonmbllem2  38449  nfdfat  38626  iccelpart  38741  2zrngmmgm  39933  opeliun2xp  40101  cbvmpt2x2  40104  ovmpt2rdxf  40107  aacllem  40527
  Copyright terms: Public domain W3C validator