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

Theorem nfan 1847
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 1846 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:    /\ wa 360   F/wnf 1554
This theorem is referenced by:  nfnan  1848  nf3an  1850  hban  1851  nfbiOLD  1858  spimtOLD  1957  cbval2OLD  1991  cbvex2  1992  nfeqfOLD  2055  nfald2  2065  dvelimfOLD  2070  nfsb4t  2129  nfsb4tOLD  2130  dvelimdfOLD  2159  sbcom  2166  sbcomOLD  2167  nfeud2  2295  mopick  2345  eupicka  2347  mopick2  2350  2eu6  2368  axbnd  2418  clelab  2558  nfel  2582  nfabd2  2592  2ralbida  2746  ralcom2  2874  reean  2876  cbvreu  2932  cbvrab  2956  ceqsex2  2994  vtocl2gaf  3020  rspce  3049  eqvincf  3066  elrabf  3093  rexab2  3103  morex  3120  reu2  3124  sbc2iegf  3229  rmo2  3248  rmo3  3250  csbiebt  3289  csbie2t  3297  cbvreucsf  3315  cbvrabcsf  3316  nfop  4002  nfopd  4003  eluniab  4029  dfnfc2  4035  nfopab  4276  cbvopab  4279  cbvopab1  4281  cbvopab2  4282  cbvopab1s  4283  mpteq12f  4288  nfmpt  4300  cbvmpt  4302  axrep3  4326  axrep4  4327  axrep5  4328  nfpo  4511  nfso  4512  nffr  4559  nfwe  4561  reusv2lem2  4728  reusv2lem3  4729  reusv6OLD  4737  onminex  4790  peano5  4871  nfxp  4907  opeliunxp  4932  nfco  5041  elrnmpt1  5122  nfimad  5215  iota2  5447  nffun  5479  imadif  5531  nffn  5544  nff  5592  nff1  5640  nffo  5655  nff1o  5675  fun11iun  5698  nffvd  5740  fv3  5747  fmptco  5904  opabex3d  5992  opabex3  5993  nfiso  6047  nfoprab  6129  mpt2eq123  6136  nfmpt2  6145  cbvoprab1  6147  cbvoprab2  6148  cbvoprab12  6149  cbvoprab3  6151  cbvmpt2x  6153  ovmpt2dxf  6202  dfoprab4f  6408  fmpt2x  6420  nfriotad  6561  cbvriota  6563  riota2df  6573  riota5f  6577  riotasv2d  6597  riotasv2dOLD  6598  riotasv2s  6599  nfrecs  6638  tfr3  6663  tz7.49  6705  erovlem  7003  nfixp  7084  nfixp1  7085  xpf1o  7272  nneneq  7293  ac6sfi  7354  nfoi  7486  wdom2d  7551  infpssrlem4  8191  hsmexlem2  8312  hsmexlem4  8314  domtriomlem  8327  axdc3lem2  8336  axdc4lem  8340  zorn2lem4  8384  zorn2lem5  8385  konigthlem  8448  axextnd  8471  axrepndlem2  8473  axrepnd  8474  axunnd  8476  axpowndlem2  8478  axpowndlem4  8480  axpownd  8481  axregndlem2  8483  axregnd  8484  axinfndlem1  8485  axinfnd  8486  zfcndrep  8494  zfcndinf  8498  nfsum1  12489  nfsum  12490  fsum2dlem  12559  fsum00  12582  mreexexd  13878  acsmapd  14609  gsum2d2lem  15552  dprd2d2  15607  neiptopnei  17201  neiptopreu  17202  neitr  17249  iunconlem  17495  iuncon  17496  ptcnplem  17658  ptcnp  17659  xkocnv  17851  isfildlem  17894  utopsnneiplem  18282  isucn2  18314  cfilucfilOLD  18604  cfilucfil  18605  restmetu  18622  ovolfiniun  19402  ovoliunlem3  19405  ovoliunnul  19408  volfiniun  19446  itg2splitlem  19643  itg2split  19644  isibl2  19661  nfitg  19669  cbvitg  19670  limciun  19786  chirred  23903  mo5f  23977  rmo3f  23987  rmo4fOLD  23988  cbvdisjf  24020  disjabrex  24029  disjabrexf  24030  funimass4f  24049  cbvmptf  24073  fmptcof2  24081  fcomptf  24082  funcnv4mpt  24090  xrofsup  24131  esumcl  24432  gsumesum  24456  esumlub  24457  esumcst  24460  esumfzf  24464  esumfsup  24465  hasheuni  24480  esumcvg  24481  measvunilem  24571  measvunilem0  24572  measvuni  24573  measinblem  24579  voliune  24590  volfiniune  24591  volmeas  24592  dstrvprob  24734  cvmcov  24955  iota5f  25187  dedekind  25192  dedekindle  25193  nfcprod1  25241  nfcprod  25242  fprod2dlem  25309  axextdist  25432  axext4dist  25433  trpredmintr  25514  nfwrecs  25538  wfrlem4  25546  nfwlim  25578  frrlem4  25590  heicant  26253  ftc1anclem5  26298  finminlem  26335  indexdom  26450  filbcmb  26456  sdclem2  26460  sdclem1  26461  fdc1  26464  mzpsubmpt  26814  mzpexpmpt  26816  eq0rabdioph  26849  eqrabdioph  26850  setindtr  27109  elunif  27677  rspcegf  27684  fnchoice  27690  refsumcn  27691  rfcnnnub  27697  fmul01  27700  fmuldfeqlem1  27702  fmuldfeq  27703  fmul01lt1lem1  27704  fmul01lt1lem2  27705  infrglb  27712  climmulf  27720  climexp  27721  climsuse  27724  climrecf  27725  climinff  27727  stoweidlem3  27742  stoweidlem26  27765  stoweidlem27  27766  stoweidlem29  27768  stoweidlem31  27770  stoweidlem34  27773  stoweidlem35  27774  stoweidlem36  27775  stoweidlem39  27778  stoweidlem42  27781  stoweidlem43  27782  stoweidlem44  27783  stoweidlem46  27785  stoweidlem48  27787  stoweidlem49  27788  stoweidlem51  27790  stoweidlem52  27791  stoweidlem53  27792  stoweidlem54  27793  stoweidlem55  27794  stoweidlem56  27795  stoweidlem57  27796  stoweidlem58  27797  stoweidlem59  27798  stoweidlem60  27799  stoweidlem61  27800  stoweidlem62  27801  stoweid  27802  wallispilem3  27806  stirlinglem13  27825  stirling  27828  nfdfat  27984  oprabv  28103  elovmpt2rab  28104  elovmpt2rab1  28105  ovmpt3rab1  28106  iunconlem2  29121  bnj919  29210  bnj1146  29236  bnj1379  29276  bnj849  29370  bnj916  29378  bnj964  29388  bnj1014  29405  bnj1123  29429  bnj1228  29454  bnj1307  29466  bnj1321  29470  bnj1398  29477  bnj1408  29479  bnj1444  29486  bnj1445  29487  bnj1446  29488  bnj1449  29491  bnj1467  29497  bnj1463  29498  bnj1489  29499  bnj1491  29500  bnj1312  29501  bnj1525  29512  nfeqfNEW7  29560  spimtNEW7  29581  nfsb4twAUX7  29650  sbcomwAUX7  29662  ax7w15lemAUX7  29741  nfald2OLD7  29791  dvelimfOLD7  29801  cbval2OLD7  29804  cbvex2OLD7  29805  nfsb4tOLD7  29819  nfsb4tw2AUXOLD7  29820  dvelimdfOLD7  29825  sbcomOLD7  29829  glbconxN  30249  pmapglb2xN  30643  cdlemefs32sn1aw  31285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator