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

Theorem nfan 1914
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 1913 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369   F/wnf 1603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-12 1840
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-nf 1604
This theorem is referenced by:  nfnan  1915  nf3an  1916  hban  1917  cbvex2OLD  2015  nfeqf  2031  nfald2  2059  nfsb4t  2116  2ax6elem  2179  eupicka  2345  mopick2  2348  2mo  2359  2moOLD  2360  2eu6OLD  2370  axbnd  2420  clelab  2587  clelabOLD  2588  nfelOLD  2619  nfabd2  2626  2ralbida  2884  r19.29an  2984  ralcom2  3008  reean  3010  cbvreu  3068  cbvrab  3093  ceqsex2  3133  vtocl2gaf  3160  rspce  3191  eqvincf  3213  elrabf  3241  elrab3t  3242  rexab2  3252  morex  3269  reu2  3273  reu2eqd  3282  sbc2iegf  3388  rmo2  3413  rmo3  3415  csbiebt  3440  csbie2t  3449  cbvreucsf  3454  cbvrabcsf  3455  rabsnifsb  4083  nfop  4218  nfopd  4219  eluniab  4245  dfnfc2  4252  rabasiun  4319  nfopab  4502  cbvopab  4505  cbvopab1  4507  cbvopab2  4508  cbvopab1s  4509  mpteq12f  4513  nfmpt  4525  cbvmpt  4527  axrep3  4551  axrep4  4552  axrep5  4553  reusv2lem2  4639  reusv2lem3  4640  reusv6OLD  4648  nfpo  4795  nfso  4796  nffr  4843  nfwe  4845  nfxp  5016  opeliunxp  5041  nfco  5158  elrnmpt1  5241  nfimad  5336  iota2  5567  nffun  5600  imadif  5653  nffn  5667  nff  5717  nff1  5769  nffo  5784  nff1o  5804  nffvd  5865  fv3  5869  fmptco  6049  nfiso  6205  nfriotad  6250  cbvriota  6252  riota2df  6263  riota5f  6267  oprabv  6330  nfoprab  6334  mpt2eq123  6341  nfmpt2  6351  cbvoprab1  6354  cbvoprab2  6355  cbvoprab12  6356  cbvoprab3  6358  cbvmpt2x  6360  ovmpt2dxf  6413  elovmpt2rab  6506  elovmpt2rab1  6507  onminex  6627  peano5  6708  fun11iun  6745  opabex3d  6763  opabex3  6764  dfoprab4f  6843  fmpt2x  6851  nfrecs  7046  tfr3  7070  tz7.49  7112  erovlem  7409  nfixp  7490  nfixp1  7491  xpf1o  7681  nneneq  7702  ac6sfi  7766  nfoi  7942  wdom2d  8009  infpssrlem4  8689  hsmexlem2  8810  hsmexlem4  8812  domtriomlem  8825  axdc3lem2  8834  axdc4lem  8838  zorn2lem4  8882  zorn2lem5  8883  konigthlem  8946  axextnd  8969  axrepndlem2  8971  axrepnd  8972  axunnd  8974  axpowndlem2  8976  axpowndlem2OLD  8977  axpowndlem4  8980  axpownd  8981  axregndlem2  8983  axregnd  8984  axregndOLD  8985  axinfndlem1  8986  axinfnd  8987  zfcndrep  8995  zfcndinf  8999  dedekind  9747  dedekindle  9748  fsuppmapnn0fiublem  12077  fsuppmapnn0fiub  12078  fsuppmapnn0fiubex  12079  nfsum1  13493  nfsum  13494  fsum2dlem  13566  fsum00  13593  nfcprod1  13698  nfcprod  13699  fprod2dlem  13765  mreexexd  15026  acsmapd  15786  gsum2d2lem  16979  dprd2d2  17071  gsummoncoe1  18324  gsummatr01lem4  19137  cpmatmcllem  19196  pmatcollpwfi  19260  cayleyhamilton1  19370  neiptopnei  19610  neiptopreu  19611  neitr  19658  iunconlem  19905  iuncon  19906  ptcnplem  20099  ptcnp  20100  xkocnv  20292  isfildlem  20335  utopsnneiplem  20727  isucn2  20759  cfilucfilOLD  21049  cfilucfil  21050  restmetu  21067  ovolfiniun  21889  ovoliunlem3  21892  ovoliunnul  21895  volfiniun  21934  itg2splitlem  22132  itg2split  22133  isibl2  22150  nfitg  22158  cbvitg  22159  limciun  22275  istrkg2ld  23834  chirred  27290  spc2ed  27348  mo5f  27359  rmo3f  27370  rmo4fOLD  27371  foresf1o  27379  cbvdisjf  27410  disjabrex  27419  disjabrexf  27420  funimass4f  27450  cbvmptf  27470  fmptcof2  27478  fcomptf  27479  funcnv4mpt  27488  cnvoprab  27522  f1od2  27523  fpwrelmap  27532  xrofsup  27558  nn0min  27588  2sqmo  27614  isarchiofld  27784  reff  27819  locfinreflem  27820  cmpcref  27830  ordtconlem1  27883  esumcl  28020  gsumesum  28044  esumlub  28045  esumcst  28048  esumfzf  28052  esumfsup  28053  hasheuni  28068  esumcvg  28069  measvunilem  28160  measvunilem0  28161  measvuni  28162  measinblem  28168  voliune  28178  volfiniune  28179  volmeas  28180  oms0  28243  eulerpartlemgvv  28292  dstrvprob  28387  cvmcov  28685  iota5f  29079  axextdist  29207  axext4dist  29208  trpredmintr  29289  nfwrecs  29313  wfrlem4  29321  nfwlim  29353  frrlem4  29365  wl-cbvalnaed  29960  wl-2sb6d  29983  wl-sbalnae  29987  wl-ax11-lem3  30002  heicant  30024  mbfposadd  30037  ftc1anclem5  30069  finminlem  30111  indexdom  30200  filbcmb  30206  sdclem2  30210  sdclem1  30211  fdc1  30214  mzpsubmpt  30650  mzpexpmpt  30652  eq0rabdioph  30685  eqrabdioph  30686  setindtr  30941  elunif  31345  rspcegf  31352  fnchoice  31358  refsumcn  31359  rfcnnnub  31365  upbdrech  31454  ssfiunibd  31458  iccshift  31494  iooshift  31498  fmul01  31502  fmuldfeqlem1  31504  fmuldfeq  31505  fmul01lt1lem1  31506  fmul01lt1lem2  31507  infrglb  31512  climmulf  31518  climexp  31519  climsuse  31522  climrecf  31523  climinff  31525  climaddf  31529  mullimc  31530  islptre  31533  climf  31536  mullimcf  31537  rexlim2d  31539  idlimc  31540  limcperiod  31542  limcrecl  31543  islpcn  31553  limsupre  31555  limcleqr  31558  addlimc  31562  limclner  31565  cncficcgt0  31598  cncfioobd  31607  iblsplitf  31659  itgperiod  31670  stoweidlem3  31674  stoweidlem26  31697  stoweidlem27  31698  stoweidlem29  31700  stoweidlem31  31702  stoweidlem34  31705  stoweidlem35  31706  stoweidlem36  31707  stoweidlem39  31710  stoweidlem42  31713  stoweidlem43  31714  stoweidlem44  31715  stoweidlem46  31717  stoweidlem48  31719  stoweidlem49  31720  stoweidlem51  31722  stoweidlem52  31723  stoweidlem53  31724  stoweidlem54  31725  stoweidlem55  31726  stoweidlem56  31727  stoweidlem57  31728  stoweidlem58  31729  stoweidlem59  31730  stoweidlem60  31731  stoweidlem61  31732  stoweidlem62  31733  stoweid  31734  wallispilem3  31738  stirlinglem13  31757  stirling  31760  fourierdlem16  31794  fourierdlem21  31799  fourierdlem22  31800  fourierdlem31  31809  fourierdlem39  31817  fourierdlem48  31826  fourierdlem51  31829  fourierdlem53  31831  fourierdlem68  31846  fourierdlem71  31849  fourierdlem73  31851  fourierdlem80  31858  fourierdlem81  31859  fourierdlem86  31864  fourierdlem87  31865  fourierdlem93  31871  fourierdlem94  31872  fourierdlem103  31881  fourierdlem104  31882  fourierdlem112  31890  fourierdlem113  31891  nfdfat  32053  2zrngmmgm  32462  opeliun2xp  32655  cbvmpt2x2  32658  ovmpt2rdxf  32661  iunconlem2  33468  bnj919  33558  bnj1146  33583  bnj1379  33622  bnj849  33716  bnj916  33724  bnj964  33734  bnj1014  33751  bnj1123  33775  bnj1228  33800  bnj1307  33812  bnj1321  33816  bnj1398  33823  bnj1408  33825  bnj1444  33832  bnj1445  33833  bnj1446  33834  bnj1449  33837  bnj1467  33843  bnj1463  33844  bnj1489  33845  bnj1491  33846  bnj1312  33847  bnj1525  33858  bj-axrep3  34124  bj-axrep4  34125  bj-axrep5  34126  riotasv2d  34428  riotasv2s  34429  glbconxN  34842  pmapglb2xN  35236  cdlemefs32sn1aw  35880
  Copyright terms: Public domain W3C validator