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

Theorem nfan 1836
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 1835 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:    /\ wa 359   F/wnf 1550
This theorem is referenced by:  nfnan  1837  nf3an  1839  hban  1840  nfbiOLD  1847  spimtOLD  1947  nfeqf  2002  nfald2  2011  dvelimf  2031  cbval2  2038  cbvex2  2039  nfsb4t  2113  dvelimdf  2115  sbcom  2122  nfeud2  2250  mopick  2300  eupicka  2302  mopick2  2305  2eu6  2323  clelab  2507  nfel  2531  nfabd2  2541  2ralbida  2688  ralcom2  2815  reean  2817  cbvreu  2873  cbvrab  2897  ceqsex2  2935  vtocl2gaf  2961  rspce  2990  eqvincf  3007  elrabf  3034  rexab2  3044  morex  3061  reu2  3065  sbc2iegf  3170  rmo2  3189  rmo3  3191  csbiebt  3230  csbie2t  3238  cbvreucsf  3256  cbvrabcsf  3257  nfop  3942  nfopd  3943  eluniab  3969  dfnfc2  3975  nfopab  4214  cbvopab  4217  cbvopab1  4219  cbvopab2  4220  cbvopab1s  4221  mpteq12f  4226  nfmpt  4238  cbvmpt  4240  axrep3  4264  axrep4  4265  axrep5  4266  nfpo  4449  nfso  4450  nffr  4497  nfwe  4499  reusv2lem2  4665  reusv2lem3  4666  reusv6OLD  4674  onminex  4727  peano5  4808  nfxp  4844  opeliunxp  4869  nfco  4978  elrnmpt1  5059  nfimad  5152  iota2  5384  nffun  5416  imadif  5468  nffn  5481  nff  5529  nff1  5577  nffo  5592  nff1o  5612  fun11iun  5635  nffvd  5677  fv3  5684  fmptco  5840  opabex3d  5928  opabex3  5929  nfiso  5983  nfoprab  6065  mpt2eq123  6072  nfmpt2  6081  cbvoprab1  6083  cbvoprab2  6084  cbvoprab12  6085  cbvoprab3  6087  cbvmpt2x  6089  ovmpt2dxf  6138  dfoprab4f  6344  fmpt2x  6356  nfriotad  6494  cbvriota  6496  riota2df  6506  riota5f  6510  riotasv2d  6530  riotasv2dOLD  6531  riotasv2s  6532  nfrecs  6571  tfr3  6596  tz7.49  6638  erovlem  6936  nfixp  7017  nfixp1  7018  xpf1o  7205  nneneq  7226  ac6sfi  7287  nfoi  7416  wdom2d  7481  infpssrlem4  8119  hsmexlem2  8240  hsmexlem4  8242  domtriomlem  8255  axdc3lem2  8264  axdc4lem  8268  zorn2lem4  8312  zorn2lem5  8313  konigthlem  8376  axextnd  8399  axrepndlem2  8401  axrepnd  8402  axunnd  8404  axpowndlem2  8406  axpowndlem4  8408  axpownd  8409  axregndlem2  8411  axregnd  8412  axinfndlem1  8413  axinfnd  8414  zfcndrep  8422  zfcndinf  8426  nfsum1  12411  nfsum  12412  fsum2dlem  12481  fsum00  12504  mreexexd  13800  acsmapd  14531  gsum2d2lem  15474  dprd2d2  15529  neiptopnei  17119  neiptopreu  17120  neitr  17166  iunconlem  17411  iuncon  17412  ptcnplem  17574  ptcnp  17575  xkocnv  17767  isfildlem  17810  utopsnneiplem  18198  isucn2  18230  cfilucfil  18479  restmetu  18489  ovolfiniun  19264  ovoliunlem3  19267  ovoliunnul  19270  volfiniun  19308  itg2splitlem  19507  itg2split  19508  isibl2  19525  nfitg  19533  cbvitg  19534  limciun  19648  chirred  23746  mo5f  23816  rmo3f  23826  rmo4fOLD  23827  cbvdisjf  23859  disjabrex  23868  disjabrexf  23869  funimass4f  23887  cbvmptf  23910  fmptcof2  23918  fcomptf  23919  funcnv4mpt  23926  xrofsup  23962  esumcl  24223  gsumesum  24247  esumlub  24248  esumcst  24251  esumfzf  24255  esumfsup  24256  hasheuni  24271  esumcvg  24272  measvunilem  24360  measvunilem0  24361  measvuni  24362  measinblem  24368  voliune  24379  volfiniune  24380  volmeas  24381  dstrvprob  24508  cvmcov  24729  iota5f  24961  dedekind  24966  dedekindle  24967  nfcprod1  25015  nfcprod  25016  axextdist  25180  axext4dist  25181  trpredmintr  25258  wfrlem4  25283  frrlem4  25308  finminlem  26012  indexdom  26127  filbcmb  26133  sdclem2  26137  sdclem1  26138  fdc1  26141  mzpsubmpt  26491  mzpexpmpt  26493  eq0rabdioph  26526  eqrabdioph  26527  setindtr  26786  elunif  27355  rspcegf  27362  fnchoice  27368  refsumcn  27369  rfcnnnub  27375  fmul01  27378  fmuldfeqlem1  27380  fmuldfeq  27381  fmul01lt1lem1  27382  fmul01lt1lem2  27383  infrglb  27390  climmulf  27398  climexp  27399  climsuse  27402  climrecf  27403  climinff  27405  stoweidlem3  27420  stoweidlem26  27443  stoweidlem27  27444  stoweidlem29  27446  stoweidlem31  27448  stoweidlem34  27451  stoweidlem35  27452  stoweidlem36  27453  stoweidlem39  27456  stoweidlem42  27459  stoweidlem43  27460  stoweidlem44  27461  stoweidlem46  27463  stoweidlem48  27465  stoweidlem49  27466  stoweidlem51  27468  stoweidlem52  27469  stoweidlem53  27470  stoweidlem54  27471  stoweidlem55  27472  stoweidlem56  27473  stoweidlem57  27474  stoweidlem58  27475  stoweidlem59  27476  stoweidlem60  27477  stoweidlem61  27478  stoweidlem62  27479  stoweid  27480  wallispilem3  27484  stirlinglem13  27503  stirling  27506  nfdfat  27663  bnj919  28474  bnj1146  28500  bnj1379  28540  bnj849  28634  bnj916  28642  bnj964  28652  bnj1014  28669  bnj1123  28693  bnj1228  28718  bnj1307  28730  bnj1321  28734  bnj1398  28741  bnj1408  28743  bnj1444  28750  bnj1445  28751  bnj1446  28752  bnj1449  28755  bnj1467  28761  bnj1463  28762  bnj1489  28763  bnj1491  28764  bnj1312  28765  bnj1525  28776  nfeqfNEW7  28824  spimtNEW7  28845  nfsb4twAUX7  28912  sbcomwAUX7  28923  nfald2OLD7  29033  dvelimfOLD7  29043  cbval2OLD7  29046  cbvex2OLD7  29047  nfsb4tOLD7  29061  nfsb4tw2AUXOLD7  29062  dvelimdfOLD7  29067  sbcomOLD7  29071  glbconxN  29492  pmapglb2xN  29886  cdlemefs32sn1aw  30528
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator