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

Theorem nfan 1875
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 1874 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600
This theorem is referenced by:  nfnan  1876  nf3an  1877  hban  1878  cbvex2OLD  2002  nfeqf  2018  nfald2  2046  nfsb4t  2103  2ax6elem  2179  nfeud2OLD  2302  mopickOLDOLD  2363  eupicka  2365  mopick2  2370  2mo  2382  2moOLD  2383  2eu6OLD  2394  axbnd  2444  clelab  2611  clelabOLD  2612  nfelOLD  2643  nfabd2  2650  2ralbida  2905  r19.29an  3002  ralcom2  3026  reean  3028  cbvreu  3086  cbvrab  3111  ceqsex2  3151  vtocl2gaf  3178  rspce  3209  eqvincf  3231  elrabf  3259  elrab3t  3260  rexab2  3270  morex  3287  reu2  3291  reu2eqd  3300  sbc2iegf  3406  rmo2  3428  rmo3  3430  csbiebt  3455  csbie2t  3464  cbvreucsf  3469  cbvrabcsf  3470  rabsnifsb  4095  nfop  4229  nfopd  4230  eluniab  4256  dfnfc2  4263  rabasiun  4329  nfopab  4512  cbvopab  4515  cbvopab1  4517  cbvopab2  4518  cbvopab1s  4519  mpteq12f  4523  nfmpt  4535  cbvmpt  4537  axrep3  4561  axrep4  4562  axrep5  4563  reusv2lem2  4649  reusv2lem3  4650  reusv6OLD  4658  nfpo  4805  nfso  4806  nffr  4853  nfwe  4855  nfxp  5026  opeliunxp  5051  nfco  5168  elrnmpt1  5251  nfimad  5346  iota2  5577  nffun  5610  imadif  5663  nffn  5677  nff  5727  nff1  5779  nffo  5794  nff1o  5814  nffvd  5875  fv3  5879  fmptco  6054  nfiso  6208  nfriotad  6253  cbvriota  6255  riota2df  6266  riota5f  6270  oprabv  6329  nfoprab  6333  mpt2eq123  6340  nfmpt2  6350  cbvoprab1  6353  cbvoprab2  6354  cbvoprab12  6355  cbvoprab3  6357  cbvmpt2x  6359  ovmpt2dxf  6412  elovmpt2rab  6505  elovmpt2rab1  6506  onminex  6626  peano5  6707  fun11iun  6744  opabex3d  6762  opabex3  6763  dfoprab4f  6842  fmpt2x  6850  nfrecs  7044  tfr3  7068  tz7.49  7110  erovlem  7407  nfixp  7488  nfixp1  7489  xpf1o  7679  nneneq  7700  ac6sfi  7764  nfoi  7939  wdom2d  8006  infpssrlem4  8686  hsmexlem2  8807  hsmexlem4  8809  domtriomlem  8822  axdc3lem2  8831  axdc4lem  8835  zorn2lem4  8879  zorn2lem5  8880  konigthlem  8943  axextnd  8966  axrepndlem2  8968  axrepnd  8969  axunnd  8971  axpowndlem2  8973  axpowndlem2OLD  8974  axpowndlem4  8977  axpownd  8978  axregndlem2  8980  axregnd  8981  axregndOLD  8982  axinfndlem1  8983  axinfnd  8984  zfcndrep  8992  zfcndinf  8996  dedekind  9743  dedekindle  9744  fsuppmapnn0fiublem  12064  fsuppmapnn0fiub  12065  fsuppmapnn0fiubex  12066  nfsum1  13475  nfsum  13476  fsum2dlem  13548  fsum00  13575  mreexexd  14903  acsmapd  15665  gsummptshft  16759  gsum2d2lem  16804  dprd2d2  16895  gsummoncoe1  18145  gsummatr01lem4  18955  cpmatmcllem  19014  pmatcollpwfi  19078  cayleyhamilton1  19188  neiptopnei  19427  neiptopreu  19428  neitr  19475  iunconlem  19722  iuncon  19723  ptcnplem  19885  ptcnp  19886  xkocnv  20078  isfildlem  20121  utopsnneiplem  20513  isucn2  20545  cfilucfilOLD  20835  cfilucfil  20836  restmetu  20853  ovolfiniun  21675  ovoliunlem3  21678  ovoliunnul  21681  volfiniun  21720  itg2splitlem  21918  itg2split  21919  isibl2  21936  nfitg  21944  cbvitg  21945  limciun  22061  istrkg2ld  23614  colline  23771  f1otrg  23878  chirred  27018  spc2ed  27076  mo5f  27087  rmo3f  27098  rmo4fOLD  27099  cbvdisjf  27135  disjabrex  27144  disjabrexf  27145  funimass4f  27175  cbvmptf  27194  fmptcof2  27202  fcomptf  27203  funcnv4mpt  27212  cnvoprab  27246  f1od2  27247  fpwrelmap  27256  xrofsup  27278  nn0min  27307  isarchi3  27421  isarchiofld  27498  ordtconlem1  27570  esumcl  27711  gsumesum  27735  esumlub  27736  esumcst  27739  esumfzf  27743  esumfsup  27744  hasheuni  27759  esumcvg  27760  measvunilem  27851  measvunilem0  27852  measvuni  27853  measinblem  27859  voliune  27869  volfiniune  27870  volmeas  27871  oms0  27934  eulerpartlemgvv  27983  dstrvprob  28078  cvmcov  28376  iota5f  28605  nfcprod1  28647  nfcprod  28648  fprod2dlem  28715  axextdist  28837  axext4dist  28838  trpredmintr  28919  nfwrecs  28943  wfrlem4  28951  nfwlim  28983  frrlem4  28995  wl-cbvalnaed  29590  wl-2sb6d  29613  wl-sbalnae  29617  wl-ax11-lem3  29632  heicant  29654  mbfposadd  29667  ftc1anclem5  29699  finminlem  29741  indexdom  29856  filbcmb  29862  sdclem2  29866  sdclem1  29867  fdc1  29870  mzpsubmpt  30307  mzpexpmpt  30309  eq0rabdioph  30342  eqrabdioph  30343  setindtr  30598  elunif  30997  rspcegf  31004  fnchoice  31010  refsumcn  31011  rfcnnnub  31017  upbdrech  31110  ssfiunibd  31114  iccshift  31150  iooshift  31154  fmul01  31158  fmuldfeqlem1  31160  fmuldfeq  31161  fmul01lt1lem1  31162  fmul01lt1lem2  31163  infrglb  31168  climmulf  31174  climexp  31175  climsuse  31178  climrecf  31179  climinff  31181  climaddf  31185  mullimc  31186  islptre  31189  climf  31192  mullimcf  31193  rexlim2d  31195  idlimc  31196  limcperiod  31198  limcrecl  31199  islpcn  31209  limsupre  31211  limcleqr  31214  addlimc  31218  limclner  31221  cncficcgt0  31255  cncfiooicc  31261  cncfioobd  31264  dvbdfbdioolem1  31286  iblsplitf  31316  itgiccshift  31326  itgperiod  31327  stoweidlem3  31331  stoweidlem26  31354  stoweidlem27  31355  stoweidlem29  31357  stoweidlem31  31359  stoweidlem34  31362  stoweidlem35  31363  stoweidlem36  31364  stoweidlem39  31367  stoweidlem42  31370  stoweidlem43  31371  stoweidlem44  31372  stoweidlem46  31374  stoweidlem48  31376  stoweidlem49  31377  stoweidlem51  31379  stoweidlem52  31380  stoweidlem53  31381  stoweidlem54  31382  stoweidlem55  31383  stoweidlem56  31384  stoweidlem57  31385  stoweidlem58  31386  stoweidlem59  31387  stoweidlem60  31388  stoweidlem61  31389  stoweidlem62  31390  stoweid  31391  wallispilem3  31395  stirlinglem13  31414  stirling  31417  fourierdlem16  31451  fourierdlem21  31456  fourierdlem22  31457  fourierdlem31  31466  fourierdlem39  31474  fourierdlem48  31483  fourierdlem51  31486  fourierdlem53  31488  fourierdlem68  31503  fourierdlem71  31506  fourierdlem73  31508  fourierdlem80  31515  fourierdlem81  31516  fourierdlem86  31521  fourierdlem87  31522  fourierdlem93  31528  fourierdlem94  31529  fourierdlem103  31538  fourierdlem104  31539  fourierdlem112  31547  fourierdlem113  31548  nfdfat  31710  opeliun2xp  32018  cbvmpt2x2  32021  ovmpt2rdxf  32024  iunconlem2  32833  bnj919  32922  bnj1146  32947  bnj1379  32986  bnj849  33080  bnj916  33088  bnj964  33098  bnj1014  33115  bnj1123  33139  bnj1228  33164  bnj1307  33176  bnj1321  33180  bnj1398  33187  bnj1408  33189  bnj1444  33196  bnj1445  33197  bnj1446  33198  bnj1449  33201  bnj1467  33207  bnj1463  33208  bnj1489  33209  bnj1491  33210  bnj1312  33211  bnj1525  33222  bj-axrep3  33475  bj-axrep4  33476  bj-axrep5  33477  riotasv2d  33778  riotasv2s  33779  glbconxN  34192  pmapglb2xN  34586  cdlemefs32sn1aw  35228
  Copyright terms: Public domain W3C validator