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

Theorem nfan 1859
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 1858 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369   F/wnf 1592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593
This theorem is referenced by:  nfnan  1860  nf3an  1861  hban  1862  cbvex2OLD  1976  nfeqf  1992  nfald2  2022  nfsb4t  2078  sbcomOLD  2118  2sb6rflem1  2159  nfeud2OLD  2278  mopickOLD  2337  eupicka  2339  mopick2  2344  2eu6  2363  axbnd  2413  clelab  2553  nfel  2577  nfabd2  2587  2ralbida  2744  ralcom2  2875  reean  2877  cbvreu  2935  cbvrab  2960  ceqsex2  2999  vtocl2gaf  3026  rspce  3057  eqvincf  3076  elrabf  3104  elrab3t  3105  rexab2  3115  morex  3132  reu2  3136  sbc2iegf  3249  rmo2  3271  rmo3  3273  csbiebt  3296  csbie2t  3304  cbvreucsf  3309  cbvrabcsf  3310  rabsnifsb  3931  nfop  4063  nfopd  4064  eluniab  4090  dfnfc2  4097  nfopab  4345  cbvopab  4348  cbvopab1  4350  cbvopab2  4351  cbvopab1s  4352  mpteq12f  4356  nfmpt  4368  cbvmpt  4370  axrep3  4394  axrep4  4395  axrep5  4396  reusv2lem2  4482  reusv2lem3  4483  reusv6OLD  4491  nfpo  4633  nfso  4634  nffr  4681  nfwe  4683  nfxp  4853  opeliunxp  4877  nfco  4992  elrnmpt1  5075  nfimad  5166  iota2  5395  nffun  5428  imadif  5481  nffn  5495  nff  5543  nff1  5592  nffo  5607  nff1o  5627  nffvd  5688  fv3  5691  fmptco  5863  nfiso  6002  nfriotad  6048  cbvriota  6050  riota2df  6061  riota5f  6065  nfoprab  6127  mpt2eq123  6134  nfmpt2  6144  cbvoprab1  6147  cbvoprab2  6148  cbvoprab12  6149  cbvoprab3  6151  cbvmpt2x  6153  ovmpt2dxf  6205  onminex  6407  peano5  6488  fun11iun  6526  opabex3d  6544  opabex3  6545  dfoprab4f  6621  fmpt2x  6629  nfrecs  6820  tfr3  6844  tz7.49  6886  erovlem  7184  nfixp  7270  nfixp1  7271  xpf1o  7461  nneneq  7482  ac6sfi  7544  nfoi  7716  wdom2d  7783  infpssrlem4  8463  hsmexlem2  8584  hsmexlem4  8586  domtriomlem  8599  axdc3lem2  8608  axdc4lem  8612  zorn2lem4  8656  zorn2lem5  8657  konigthlem  8720  axextnd  8743  axrepndlem2  8745  axrepnd  8746  axunnd  8748  axpowndlem2  8750  axpowndlem2OLD  8751  axpowndlem4  8754  axpownd  8755  axregndlem2  8757  axregnd  8758  axinfndlem1  8759  axinfnd  8760  zfcndrep  8768  zfcndinf  8772  dedekind  9520  dedekindle  9521  nfsum1  13150  nfsum  13151  fsum2dlem  13220  fsum00  13243  mreexexd  14568  acsmapd  15330  gsum2d2lem  16438  dprd2d2  16516  gsummatr01lem4  18305  neiptopnei  18577  neiptopreu  18578  neitr  18625  iunconlem  18872  iuncon  18873  ptcnplem  19035  ptcnp  19036  xkocnv  19228  isfildlem  19271  utopsnneiplem  19663  isucn2  19695  cfilucfilOLD  19985  cfilucfil  19986  restmetu  20003  ovolfiniun  20825  ovoliunlem3  20828  ovoliunnul  20831  volfiniun  20869  itg2splitlem  21067  itg2split  21068  isibl2  21085  nfitg  21093  cbvitg  21094  limciun  21210  colline  22917  f1otrg  22939  chirred  25621  spc2ed  25679  mo5f  25691  rmo3f  25702  rmo4fOLD  25703  cbvdisjf  25740  disjabrex  25749  disjabrexf  25750  funimass4f  25774  cbvmptf  25794  fmptcof2  25802  fcomptf  25803  funcnv4mpt  25812  cnvoprab  25846  f1od2  25847  fpwrelmap  25857  xrofsup  25877  nn0min  25912  isarchi3  26027  isarchiofld  26137  ordtconlem1  26207  esumcl  26339  gsumesum  26363  esumlub  26364  esumcst  26367  esumfzf  26371  esumfsup  26372  hasheuni  26387  esumcvg  26388  measvunilem  26479  measvunilem0  26480  measvuni  26481  measinblem  26487  voliune  26498  volfiniune  26499  volmeas  26500  eulerpartlemgvv  26606  dstrvprob  26701  cvmcov  26999  iota5f  27227  nfcprod1  27269  nfcprod  27270  fprod2dlem  27337  axextdist  27459  axext4dist  27460  trpredmintr  27541  nfwrecs  27565  wfrlem4  27573  nfwlim  27605  frrlem4  27617  wl-cbvalnaed  28207  wl-2sb6d  28230  wl-sbalnae  28234  wl-ax11-lem3  28244  heicant  28267  mbfposadd  28280  ftc1anclem5  28312  finminlem  28354  indexdom  28469  filbcmb  28475  sdclem2  28479  sdclem1  28480  fdc1  28483  mzpsubmpt  28921  mzpexpmpt  28923  eq0rabdioph  28957  eqrabdioph  28958  setindtr  29215  elunif  29580  rspcegf  29587  fnchoice  29593  refsumcn  29594  rfcnnnub  29600  fmul01  29603  fmuldfeqlem1  29605  fmuldfeq  29606  fmul01lt1lem1  29607  fmul01lt1lem2  29608  infrglb  29614  climmulf  29620  climexp  29621  climsuse  29624  climrecf  29625  climinff  29627  stoweidlem3  29641  stoweidlem26  29664  stoweidlem27  29665  stoweidlem29  29667  stoweidlem31  29669  stoweidlem34  29672  stoweidlem35  29673  stoweidlem36  29674  stoweidlem39  29677  stoweidlem42  29680  stoweidlem43  29681  stoweidlem44  29682  stoweidlem46  29684  stoweidlem48  29686  stoweidlem49  29687  stoweidlem51  29689  stoweidlem52  29690  stoweidlem53  29691  stoweidlem54  29692  stoweidlem55  29693  stoweidlem56  29694  stoweidlem57  29695  stoweidlem58  29696  stoweidlem59  29697  stoweidlem60  29698  stoweidlem61  29699  stoweidlem62  29700  stoweid  29701  wallispilem3  29705  stirlinglem13  29724  stirling  29727  nfdfat  29879  oprabv  30000  elovmpt2rab  30001  elovmpt2rab1  30002  rabasiun  30073  opeliun2xp  30562  cbvmpt2x2  30567  ovmpt2rdxf  30570  iunconlem2  31370  bnj919  31459  bnj1146  31484  bnj1379  31523  bnj849  31617  bnj916  31625  bnj964  31635  bnj1014  31652  bnj1123  31676  bnj1228  31701  bnj1307  31713  bnj1321  31717  bnj1398  31724  bnj1408  31726  bnj1444  31733  bnj1445  31734  bnj1446  31735  bnj1449  31738  bnj1467  31744  bnj1463  31745  bnj1489  31746  bnj1491  31747  bnj1312  31748  bnj1525  31759  bj-axrep3  31928  bj-axrep4  31929  bj-axrep5  31930  riotasv2d  32178  riotasv2s  32179  glbconxN  32592  pmapglb2xN  32986  cdlemefs32sn1aw  33628
  Copyright terms: Public domain W3C validator