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

Theorem nfan 2031
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 2030 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 376   F/wnf 1675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676
This theorem is referenced by:  nfnan  2032  nf3an  2033  hban  2034  nfeqf  2152  nfald2  2180  nfsb4t  2238  2ax6elem  2298  eupicka  2386  mopick2  2389  2mo  2400  axbnd  2450  clelab  2596  nfabd2  2631  2ralbida  2830  r19.29an  2917  ralcom2  2941  reean  2943  cbvreu  3003  cbvrab  3029  ceqsex2  3072  vtocl2gaf  3100  rspce  3131  eqvincf  3155  elrabf  3182  elrab3t  3183  rexab2  3193  morex  3210  reu2  3214  reu2eqd  3223  sbc2iegf  3322  rmo2  3342  rmo3  3344  csbiebt  3369  csbie2t  3378  cbvreucsf  3383  cbvrabcsf  3384  rabsnifsb  4031  nfop  4174  nfopd  4175  eluniab  4201  dfnfc2  4208  rabasiun  4273  nfopab  4461  cbvopab  4464  cbvopab1  4466  cbvopab2  4467  cbvopab1s  4468  mpteq12f  4472  nfmpt  4484  cbvmptf  4486  cbvmpt  4487  axrep3  4511  axrep4  4512  axrep5  4513  reusv2lem2  4603  reusv2lem3  4604  nfpo  4765  nfso  4766  nffr  4813  nfwe  4815  nfxp  4866  opeliunxp  4891  nfco  5005  elrnmpt1  5089  nfimad  5183  elsnxp  5385  iota2  5579  nffun  5611  imadif  5668  nffn  5682  nff  5735  nff1  5790  nffo  5805  nff1o  5826  nffvd  5888  fv3  5892  fmptco  6072  fsnex  6199  nfiso  6233  nfriotad  6278  cbvriota  6280  riota2df  6290  riota5f  6294  oprabv  6358  nfoprab  6362  mpt2eq123  6369  nfmpt2  6379  cbvoprab1  6382  cbvoprab2  6383  cbvoprab12  6384  cbvoprab3  6386  cbvmpt2x  6388  ovmpt2dxf  6441  elovmpt2rab  6534  elovmpt2rab1  6535  onminex  6653  peano5  6735  fun11iun  6772  opabex3d  6790  opabex3  6791  dfoprab4f  6870  fmpt2x  6878  opeliunxp2f  6975  nfwrecs  7048  wfrlem4  7057  tfr3  7135  tz7.49  7180  erovlem  7477  nfixp  7559  nfixp1  7560  xpf1o  7752  nneneq  7773  ac6sfi  7833  nfoi  8047  wdom2d  8113  infpssrlem4  8754  hsmexlem2  8875  hsmexlem4  8877  domtriomlem  8890  axdc3lem2  8899  axdc4lem  8903  zorn2lem4  8947  zorn2lem5  8948  konigthlem  9011  axextnd  9034  axrepndlem2  9036  axrepnd  9037  axunnd  9039  axpowndlem2  9041  axpowndlem4  9043  axpownd  9044  axregndlem2  9046  axregnd  9047  axinfndlem1  9048  axinfnd  9049  zfcndrep  9057  zfcndinf  9061  dedekind  9815  dedekindle  9816  fsuppmapnn0fiublem  12240  fsuppmapnn0fiub  12241  fsuppmapnn0fiubex  12242  nfsum1  13833  nfsum  13834  fsum2dlem  13908  fsum00  13935  nfcprod1  14041  nfcprod  14042  fprod2dlem  14111  fprodsplitf  14119  fprodsplit1f  14121  fprodle  14127  lcmfunsnlem1  14689  lcmfunsnlem2lem1  14690  lcmfunsnlem2  14692  mreexexd  15632  acsmapd  16502  gsum2d2lem  17683  dprd2d2  17755  gsummoncoe1  18975  gsummatr01lem4  19760  cpmatmcllem  19819  pmatcollpwfi  19883  cayleyhamilton1  19993  neiptopnei  20225  neiptopreu  20226  neitr  20273  iunconlem  20519  iuncon  20520  ptcnplem  20713  ptcnp  20714  xkocnv  20906  isfildlem  20950  utopsnneiplem  21340  isucn2  21372  cfilucfil  21652  restmetu  21663  ovolfiniun  22532  ovoliunlem3  22535  ovoliunnul  22538  volfiniun  22579  itg2splitlem  22785  itg2split  22786  isibl2  22803  nfitg  22811  cbvitg  22812  limciun  22928  istrkg2ld  24587  chirred  28129  spc2ed  28187  mo5f  28199  rmo3f  28210  rmo4fOLD  28211  foresf1o  28218  cbvdisjf  28259  disjabrex  28269  disjabrexf  28270  funimass4f  28310  fmptcof2  28334  fcomptf  28335  acunirnmpt2  28337  acunirnmpt2f  28338  aciunf1lem  28339  funcnv4mpt  28348  cnvoprab  28383  f1od2  28384  fpwrelmap  28393  xrofsup  28428  nn0min  28459  2sqmo  28485  isarchiofld  28654  reff  28740  locfinreflem  28741  cmpcref  28751  ordtconlem1  28804  esumcl  28925  gsumesum  28954  esumlub  28955  esumcst  28958  esumrnmpt2  28963  esumfzf  28964  esumfsup  28965  hasheuni  28980  esumcvg  28981  esumgect  28985  esumcvgre  28986  esum2dlem  28987  esum2d  28988  esumiun  28989  ldsysgenld  29056  sigapildsyslem  29057  sigapildsys  29058  ldgenpisyslem1  29059  measvunilem  29108  measvunilem0  29109  measvuni  29110  measinblem  29116  voliune  29125  volfiniune  29126  volmeas  29127  oms0  29198  omssubadd  29201  oms0OLD  29202  omssubaddOLD  29205  eulerpartlemgvv  29282  dstrvprob  29377  bnj919  29650  bnj1146  29675  bnj1379  29714  bnj849  29808  bnj916  29816  bnj964  29826  bnj1014  29843  bnj1123  29867  bnj1228  29892  bnj1307  29904  bnj1321  29908  bnj1398  29915  bnj1408  29917  bnj1444  29924  bnj1445  29925  bnj1446  29926  bnj1449  29929  bnj1467  29935  bnj1463  29936  bnj1489  29937  bnj1491  29938  bnj1312  29939  bnj1525  29950  cvmcov  30058  iota5f  30429  axextdist  30517  axext4dist  30518  trpredmintr  30543  nfwlim  30576  frrlem4  30588  finminlem  31045  bj-axrep3  31471  bj-axrep4  31472  bj-axrep5  31473  isbasisrelowllem1  31828  isbasisrelowllem2  31829  wl-cbvalnaed  31935  wl-2sb6d  31958  wl-sbalnae  31962  wl-mo2tf  31970  wl-eutf  31972  wl-ax11-lem3  31981  phpreu  31993  poimirlem26  32030  poimirlem27  32031  heicant  32039  mbfposadd  32052  ftc1anclem5  32085  indexdom  32125  filbcmb  32131  sdclem2  32135  sdclem1  32136  fdc1  32139  riotasv2d  32593  riotasv2s  32594  nfded2  32605  glbconxN  33014  pmapglb2xN  33408  cdlemefs32sn1aw  34052  mzpsubmpt  35656  mzpexpmpt  35658  eq0rabdioph  35690  eqrabdioph  35691  setindtr  35950  ss2iundf  36322  binomcxplemnotnn0  36775  iunconlem2  37395  elunif  37400  rspcegf  37407  fnchoice  37413  refsumcn  37414  rfcnnnub  37420  uzwo4  37451  fiiuncl  37465  rspcef  37475  disjf1  37528  wessf1ornlem  37530  disjrnmpt2  37534  disjf1o  37537  fompt  37538  disjinfi  37539  choicefi  37552  upbdrech  37611  ssfiunibd  37615  supxrgere  37643  supxrgelem  37647  supxrge  37648  xralrple2  37664  infxr  37677  infxrunb2  37678  iccshift  37715  iooshift  37719  fsumclf  37741  fsumsplitf  37742  fsummulc1f  37743  fsumsplit1  37747  fsumf1of  37749  fsumreclf  37751  fsumlessf  37752  fmul01  37755  fmuldfeqlem1  37757  fmuldfeq  37758  fmul01lt1lem1  37759  fmul01lt1lem2  37760  infrglbOLD  37766  fprodexp  37771  mccl  37775  climmulf  37779  climexp  37780  climsuse  37784  climrecf  37785  climinff  37787  climinffOLD  37788  climaddf  37792  mullimc  37793  islptre  37796  climf  37799  mullimcf  37800  rexlim2d  37802  idlimc  37803  limcperiod  37805  limcrecl  37806  islpcn  37816  limsupre  37818  limsupreOLD  37819  limcleqr  37822  addlimc  37826  limclner  37829  cncficcgt0  37863  cncfioobd  37872  dvmptmulf  37909  dvnmul  37915  dvmptfprodlem  37916  dvmptfprod  37917  dvnprodlem1  37918  dvnprodlem2  37919  iblsplitf  37944  itgperiod  37955  stoweidlem3  37975  stoweidlem26  37998  stoweidlem27  37999  stoweidlem29  38001  stoweidlem29OLD  38002  stoweidlem31  38004  stoweidlem34  38007  stoweidlem35  38008  stoweidlem36  38009  stoweidlem39  38012  stoweidlem42  38015  stoweidlem43  38016  stoweidlem44  38017  stoweidlem46  38019  stoweidlem48  38021  stoweidlem49  38022  stoweidlem51  38024  stoweidlem52  38025  stoweidlem53  38026  stoweidlem54  38027  stoweidlem55  38028  stoweidlem56  38029  stoweidlem57  38030  stoweidlem58  38031  stoweidlem59  38032  stoweidlem60  38033  stoweidlem61  38034  stoweidlem62  38035  stoweidlem62OLD  38036  stoweid  38037  wallispilem3  38041  stirlinglem13  38060  stirling  38063  fourierdlem16  38097  fourierdlem21  38102  fourierdlem22  38103  fourierdlem31  38112  fourierdlem31OLD  38113  fourierdlem39  38121  fourierdlem48  38130  fourierdlem51  38133  fourierdlem53  38135  fourierdlem68  38150  fourierdlem71  38153  fourierdlem73  38155  fourierdlem80  38162  fourierdlem81  38163  fourierdlem86  38168  fourierdlem87  38169  fourierdlem93  38175  fourierdlem94  38176  fourierdlem103  38185  fourierdlem104  38186  fourierdlem112  38194  fourierdlem113  38195  elaa2  38211  etransclem32  38243  salexct  38305  sge0revalmpt  38334  sge0f1o  38338  sge0lefi  38354  sge0resplit  38362  sge0lempt  38366  sge0iunmptlemre  38371  sge0fodjrnlem  38372  sge0iunmpt  38374  sge0ltfirpmpt2  38382  sge0isum  38383  sge0xp  38385  sge0isummpt2  38388  sge0xadd  38391  sge0pnffsumgt  38398  sge0gtfsumgt  38399  sge0uzfsumgt  38400  iundjiun  38414  meadjiun  38420  ismeannd  38421  voliunsge0lem  38426  caragenfiiuncl  38455  omeiunltfirp  38459  ovnsubaddlem2  38511  hoidmvval0  38527  hoidmvlelem1  38535  hoidmvlelem3  38537  hoidmvlelem5  38539  ovnlecvr2  38550  hspdifhsp  38556  hoiqssbllem2  38563  hoiqssbllem3  38564  hspmbllem2  38567  opnvonmbllem2  38573  nfdfat  38777  iccelpart  38892  2zrngmmgm  40454  opeliun2xp  40622  cbvmpt2x2  40625  ovmpt2rdxf  40628  aacllem  41046
  Copyright terms: Public domain W3C validator