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

Theorem nfan 1846
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 1845 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:    /\ wa 359   F/wnf 1553
This theorem is referenced by:  nfnan  1847  nf3an  1849  hban  1850  nfbiOLD  1857  spimtOLD  1956  cbval2OLD  1990  cbvex2  1991  nfeqfOLD  2050  nfald2  2060  dvelimfOLD  2065  nfsb4t  2154  nfsb4tOLD  2155  dvelimdfOLD  2157  sbcom  2164  nfeud2  2292  mopick  2342  eupicka  2344  mopick2  2347  2eu6  2365  axbnd  2415  clelab  2555  nfel  2579  nfabd2  2589  2ralbida  2736  ralcom2  2864  reean  2866  cbvreu  2922  cbvrab  2946  ceqsex2  2984  vtocl2gaf  3010  rspce  3039  eqvincf  3056  elrabf  3083  rexab2  3093  morex  3110  reu2  3114  sbc2iegf  3219  rmo2  3238  rmo3  3240  csbiebt  3279  csbie2t  3287  cbvreucsf  3305  cbvrabcsf  3306  nfop  3992  nfopd  3993  eluniab  4019  dfnfc2  4025  nfopab  4265  cbvopab  4268  cbvopab1  4270  cbvopab2  4271  cbvopab1s  4272  mpteq12f  4277  nfmpt  4289  cbvmpt  4291  axrep3  4315  axrep4  4316  axrep5  4317  nfpo  4500  nfso  4501  nffr  4548  nfwe  4550  reusv2lem2  4717  reusv2lem3  4718  reusv6OLD  4726  onminex  4779  peano5  4860  nfxp  4896  opeliunxp  4921  nfco  5030  elrnmpt1  5111  nfimad  5204  iota2  5436  nffun  5468  imadif  5520  nffn  5533  nff  5581  nff1  5629  nffo  5644  nff1o  5664  fun11iun  5687  nffvd  5729  fv3  5736  fmptco  5893  opabex3d  5981  opabex3  5982  nfiso  6036  nfoprab  6118  mpt2eq123  6125  nfmpt2  6134  cbvoprab1  6136  cbvoprab2  6137  cbvoprab12  6138  cbvoprab3  6140  cbvmpt2x  6142  ovmpt2dxf  6191  dfoprab4f  6397  fmpt2x  6409  nfriotad  6550  cbvriota  6552  riota2df  6562  riota5f  6566  riotasv2d  6586  riotasv2dOLD  6587  riotasv2s  6588  nfrecs  6627  tfr3  6652  tz7.49  6694  erovlem  6992  nfixp  7073  nfixp1  7074  xpf1o  7261  nneneq  7282  ac6sfi  7343  nfoi  7475  wdom2d  7540  infpssrlem4  8178  hsmexlem2  8299  hsmexlem4  8301  domtriomlem  8314  axdc3lem2  8323  axdc4lem  8327  zorn2lem4  8371  zorn2lem5  8372  konigthlem  8435  axextnd  8458  axrepndlem2  8460  axrepnd  8461  axunnd  8463  axpowndlem2  8465  axpowndlem4  8467  axpownd  8468  axregndlem2  8470  axregnd  8471  axinfndlem1  8472  axinfnd  8473  zfcndrep  8481  zfcndinf  8485  nfsum1  12476  nfsum  12477  fsum2dlem  12546  fsum00  12569  mreexexd  13865  acsmapd  14596  gsum2d2lem  15539  dprd2d2  15594  neiptopnei  17188  neiptopreu  17189  neitr  17236  iunconlem  17482  iuncon  17483  ptcnplem  17645  ptcnp  17646  xkocnv  17838  isfildlem  17881  utopsnneiplem  18269  isucn2  18301  cfilucfilOLD  18591  cfilucfil  18592  restmetu  18609  ovolfiniun  19389  ovoliunlem3  19392  ovoliunnul  19395  volfiniun  19433  itg2splitlem  19632  itg2split  19633  isibl2  19650  nfitg  19658  cbvitg  19659  limciun  19773  chirred  23890  mo5f  23964  rmo3f  23974  rmo4fOLD  23975  cbvdisjf  24007  disjabrex  24016  disjabrexf  24017  funimass4f  24036  cbvmptf  24060  fmptcof2  24068  fcomptf  24069  funcnv4mpt  24077  xrofsup  24118  esumcl  24419  gsumesum  24443  esumlub  24444  esumcst  24447  esumfzf  24451  esumfsup  24452  hasheuni  24467  esumcvg  24468  measvunilem  24558  measvunilem0  24559  measvuni  24560  measinblem  24566  voliune  24577  volfiniune  24578  volmeas  24579  dstrvprob  24721  cvmcov  24942  iota5f  25174  dedekind  25179  dedekindle  25180  nfcprod1  25228  nfcprod  25229  fprod2dlem  25296  axextdist  25419  axext4dist  25420  trpredmintr  25501  nfwrecs  25525  wfrlem4  25533  nfwlim  25565  frrlem4  25577  finminlem  26302  indexdom  26417  filbcmb  26423  sdclem2  26427  sdclem1  26428  fdc1  26431  mzpsubmpt  26781  mzpexpmpt  26783  eq0rabdioph  26816  eqrabdioph  26817  setindtr  27076  elunif  27644  rspcegf  27651  fnchoice  27657  refsumcn  27658  rfcnnnub  27664  fmul01  27667  fmuldfeqlem1  27669  fmuldfeq  27670  fmul01lt1lem1  27671  fmul01lt1lem2  27672  infrglb  27679  climmulf  27687  climexp  27688  climsuse  27691  climrecf  27692  climinff  27694  stoweidlem3  27709  stoweidlem26  27732  stoweidlem27  27733  stoweidlem29  27735  stoweidlem31  27737  stoweidlem34  27740  stoweidlem35  27741  stoweidlem36  27742  stoweidlem39  27745  stoweidlem42  27748  stoweidlem43  27749  stoweidlem44  27750  stoweidlem46  27752  stoweidlem48  27754  stoweidlem49  27755  stoweidlem51  27757  stoweidlem52  27758  stoweidlem53  27759  stoweidlem54  27760  stoweidlem55  27761  stoweidlem56  27762  stoweidlem57  27763  stoweidlem58  27764  stoweidlem59  27765  stoweidlem60  27766  stoweidlem61  27767  stoweidlem62  27768  stoweid  27769  wallispilem3  27773  stirlinglem13  27792  stirling  27795  nfdfat  27951  iunconlem2  28974  bnj919  29063  bnj1146  29089  bnj1379  29129  bnj849  29223  bnj916  29231  bnj964  29241  bnj1014  29258  bnj1123  29282  bnj1228  29307  bnj1307  29319  bnj1321  29323  bnj1398  29330  bnj1408  29332  bnj1444  29339  bnj1445  29340  bnj1446  29341  bnj1449  29344  bnj1467  29350  bnj1463  29351  bnj1489  29352  bnj1491  29353  bnj1312  29354  bnj1525  29365  nfeqfNEW7  29413  spimtNEW7  29434  nfsb4twAUX7  29503  sbcomwAUX7  29515  ax7w15lemAUX7  29594  nfald2OLD7  29644  dvelimfOLD7  29654  cbval2OLD7  29657  cbvex2OLD7  29658  nfsb4tOLD7  29672  nfsb4tw2AUXOLD7  29673  dvelimdfOLD7  29678  sbcomOLD7  29682  glbconxN  30102  pmapglb2xN  30496  cdlemefs32sn1aw  31138
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator