Theorem ad2antrr 488

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad2antrr	⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem ad2antrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantlr 477	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad3antrrr  492  ad5ant13  519  ad5ant23  522  simpll  527  simplll  535  simpllr  536  ad5ant123  1266  vtoclgft  2865  reupick  3505  euotd  4371  frirrg  4471  ralxfrd  4583  nnsucpred  4739  foun  5633  f1oprg  5660  dffo4  5825  funopsn  5860  foeqcnvco  5963  fliftfun  5969  isotr  5989  riotass2  6032  ovmpodxf  6179  suppfnss  6457  suppcofn  6466  mpoxopoveq  6471  tfrlem1  6539  tfrlemibacc  6557  tfrlemibfn  6559  tfrlemi14d  6564  tfrexlem  6565  tfr1onlembacc  6573  tfr1onlembfn  6575  tfr1onlemres  6580  tfrcllembacc  6586  tfrcllembfn  6588  tfrcllemres  6593  frecabcl  6630  nnmordi  6749  eroprf  6862  mapsnd  6923  f1imaen2g  7033  pw2f1odclem  7087  xpen  7098  mapen  7099  mapdom1g  7100  mapxpen  7101  xpmapenlem  7102  phplem4dom  7116  nndomo  7118  phpm  7120  fidifsnen  7125  dif1enen  7137  fisbth  7140  fimax2gtrilemstep  7158  fimax2gtri  7159  eqsndc  7163  en2eqpr  7167  unsnfidcex  7180  unsnfidcel  7181  ssfirab  7197  fidcenumlemrks  7223  sbthlemi8  7234  fiuni  7265  2omap  7269  ordiso2  7326  updjud  7373  difinfsnlem  7390  ctssdclemn0  7401  ctssdccl  7402  ctssdc  7404  enumctlemm  7405  enumct  7406  nnnninfeq  7419  nninfisol  7424  enomnilem  7429  fodju0  7438  enmkvlem  7452  enwomnilem  7460  nninfwlpoimlemg  7466  pr1or2  7491  pr2cv1  7492  exmidfodomrlemim  7504  exmidontriimlem2  7529  exmidapne  7574  cc3  7582  dfplpq2  7669  nqpi  7693  nqnq0pi  7753  nq0nn  7757  elinp  7789  elnp1st2nd  7791  genprndl  7836  genprndu  7837  addnqprllem  7842  addnqprulem  7843  addnqprl  7844  addnqpru  7845  addlocpr  7851  nqprloc  7860  prmuloc  7881  mulnqprl  7883  mulnqpru  7884  mullocpr  7886  distrlem1prl  7897  distrlem1pru  7898  ltsopr  7911  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemloc  7922  ltexprlemrl  7925  ltexprlemru  7927  addcanprleml  7929  addcanprlemu  7930  recexprlemloc  7946  recexprlem1ssl  7948  recexprlem1ssu  7949  aptiprleml  7954  aptiprlemu  7955  archpr  7958  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlemladdru  7971  archrecpr  7979  caucvgprlemnkj  7981  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemladdfu  7992  caucvgprprlemnkltj  8004  caucvgprprlemnkeqj  8005  caucvgprprlemnjltk  8006  caucvgprprlemml  8009  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemdisj  8017  caucvgprprlemexbt  8021  caucvgprprlemexb  8022  caucvgprprlemaddq  8023  suplocexprlemru  8034  suplocexprlemloc  8036  suplocexprlemex  8037  suplocexprlemub  8038  suplocexprlemlub  8039  mulgt0sr  8093  caucvgsrlemcau  8108  caucvgsrlemoffcau  8113  caucvgsrlemoffres  8115  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  axcaucvglemcau  8213  axcaucvglemres  8214  axpre-suploclemres  8216  axsuploc  8346  cnegexlem1  8448  cnegex  8451  apsym  8880  apcotr  8881  apadd1  8882  mulext1  8886  mulge0  8893  apti  8896  aprcl  8920  conjmulap  9003  lemulge11  9140  creui  9234  nndiv  9278  zaddcllemneg  9616  suprzclex  9676  eluzuzle  9862  infregelbex  9930  divfnzn  9953  qapne  9971  xrltso  10129  xnn0dcle  10135  xnn0letri  10136  xrre  10153  xrre3  10155  xaddf  10177  xaddval  10178  xpncan  10204  xleadd1a  10206  xltadd1  10209  xleaddadd  10220  ixxss12  10239  elioc2  10269  elico2  10270  elicc2  10271  fzm1  10434  fzneuz  10435  eluzgtdifelfzo  10542  elfzonelfzo  10575  exfzdc  10586  zsupcllemstep  10589  infssuzex  10593  suprzubdc  10596  nninfdcex  10597  zsupssdc  10598  qtri3or  10600  exbtwnzlemstep  10607  exbtwnzlemex  10609  exbtwnz  10610  modqid  10711  modqcyc2  10722  modqmuladd  10728  modqmuladdnn0  10730  modaddmodlo  10750  addmodlteq  10760  frecuzrdgrrn  10770  frec2uzrdg  10771  frecuzrdgsuc  10776  frecuzrdgsuctlem  10785  nninfinf  10805  seq3clss  10833  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemab  10864  iseqf1olemmo  10867  iseqf1olemqf1o  10868  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  seq3f1olemp  10877  seq3f1oleml  10878  seq3f1o  10879  seqf1oglem1  10881  seqf1oglem2  10882  seqf1og  10883  seq3id3  10886  seqfeq4g  10893  ser3ge0  10898  exp3val  10903  expap0  10931  qsqeqor  11012  modqexp  11028  nn0ltexp2  11071  facndiv  11101  faclbnd  11103  bcval5  11125  hashunlem  11168  hashun  11169  hashprg  11173  fiprsshashgt1  11182  hashfacen  11208  zfz1isolemiso  11211  zfz1isolem1  11212  seq3coll  11214  hashtpglem  11218  ccatcl  11281  ccatlen  11283  ccatvalfn  11289  ccatsymb  11290  ccatrn  11297  ccat2s1fstg  11336  swrdclg  11342  swrdspsleq  11359  pfxeq  11388  swrdswrd  11397  wrdind  11414  wrd2ind  11415  swrdccatin1  11417  swrdccatin2  11421  pfxccatin12  11425  pfxccat3  11426  swrdccat3b  11432  reuccatpfxs1  11439  ovshftex  11504  2shfti  11516  seq3shft  11523  cjap  11591  caucvgrelemcau  11665  cvg1nlemcau  11669  cvg1nlemres  11670  recvguniq  11680  resqrexlemdecn  11697  resqrexlemcalc3  11701  resqrexlemcvg  11704  resqrexlemoverl  11706  leabs  11759  absexpzap  11765  ltabs  11772  abslt  11773  absle  11774  maxleim  11890  maxabslemval  11893  fimaxre2  11912  minmax  11915  2zinfmin  11928  xrmaxiflemcl  11930  xrmaxifle  11931  xrmaxiflemab  11932  xrmaxiflemlub  11933  xrmaxiflemcom  11934  xrmaxltsup  11943  xrmaxadd  11946  xrminmax  11950  xrbdtri  11961  2clim  11986  climshftlemg  11987  climsqz  12020  climsqz2  12021  climrecvg1n  12033  climcvg1nlem  12034  serf0  12037  sumrbdclem  12063  fsum3cvg  12064  summodclem3  12066  summodclem2a  12067  summodclem2  12068  zsumdc  12070  fsum3  12073  isumss  12077  fisumss  12078  fsum3cvg3  12082  fsumcl2lem  12084  fsumadd  12092  fsumsplit  12093  sumsnf  12095  fsum2d  12121  fisum0diag2  12133  fsummulc2  12134  modfsummod  12144  fsumabs  12151  fsumrelem  12157  fsumiun  12163  geoisumr  12204  cvgratnnlemseq  12212  cvgratz  12218  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  prodrbdclem  12257  fproddccvg  12258  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  fprodntrivap  12270  fprodssdc  12276  fprodmul  12277  prodsnf  12278  fprodsplitdc  12282  fprodsplit  12283  fprodunsn  12290  fprodcl2lem  12291  fprodap0  12307  fprod2d  12309  fprodrec  12315  fprodap0f  12322  efcj  12359  efaddlem  12360  tanaddaplem  12424  sinltxirr  12447  nndivides  12483  dvdsext  12541  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  bitsfzolem  12640  bitsmod  12642  bitsinv1  12648  dvdsbnd  12652  bezoutlemnewy  12692  bezoutlemstep  12693  bezoutlemmain  12694  bezoutlemzz  12698  bezoutlemaz  12699  bezoutlembz  12700  bezoutlemeu  12703  bezoutlemle  12704  bezoutlemsup  12705  dfgcd3  12706  dfgcd2  12710  bezoutr1  12729  nnmindc  12730  nninfctlemfo  12736  dvdslcm  12766  lcmgcdlem  12774  qredeq  12793  qredeu  12794  divgcdcoprm0  12798  divgcdcoprmex  12799  cncongr1  12800  isprm2lem  12813  prmind2  12817  exprmfct  12835  prmdvdsfz  12836  isprm5lem  12838  prmexpb  12848  rpexp1i  12851  sqrt2irr  12859  sqne2sq  12874  nonsq  12904  phiprmpw  12919  eulerthlemrprm  12926  eulerthlema  12927  hashgcdeq  12937  phisum  12938  modprmn0modprm0  12954  pclemub  12985  pclemdc  12986  pcmul  12999  pcqmul  13001  pcxqcl  13010  pcdvdstr  13025  pcprmpw2  13031  difsqpwdvds  13036  pcmpt  13041  oddprmdvds  13052  prmpwdvds  13053  pockthg  13055  infpnlem1  13057  1arith  13065  4sqlem2  13087  4sqlemafi  13093  4sqlemffi  13094  4sqleminfi  13095  4sqlem11  13099  4sqlem13m  13101  4sqlem14  13102  4sqlem17  13105  4sqlem18  13106  ennnfonelemg  13154  ennnfoneleminc  13162  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemfun  13168  ennnfonelemf1  13169  ennnfonelemrn  13170  ennnfonelemdm  13171  ennnfonelemnn0  13173  ennnfonelemim  13175  exmidunben  13177  ctinfomlemom  13178  ctinf  13181  ctiunctlemudc  13188  nninfdclemlt  13202  nninfdclemf1  13203  isstruct2r  13223  prdsval  13486  imasival  13519  gsumpropd2  13606  sgrppropd  13626  prdssgrpd  13628  mndpropd  13653  issubmnd  13655  prdsidlem  13660  prdsmndd  13661  pws0g  13664  mndissubm  13688  resmhm2b  13702  mhmeql  13705  gsumfzz  13708  gsumwsubmcl  13709  gsumwmhm  13711  gsumfzcl  13712  grpinvnz  13784  pwssub  13826  mhmmnd  13833  mulgfng  13841  mulgz  13867  mulgnndir  13868  mulgnn0dir  13869  mulgneg2  13873  mulgass  13876  mhmmulg  13880  issubgrpd2  13907  issubg4m  13910  grpissubg  13911  isnsg3  13924  ghmpreima  13983  ghmnsgpreima  13986  ghmf1  13990  conjnmz  13996  conjnmzb  13997  eqgabl  14047  gsumfzreidx  14054  gsumfzsubmcl  14055  gsumfzmptfidmadd  14056  gsumfzmhm  14060  rngpropd  14099  issrg  14109  ringpropd  14182  ringinvnz1ne0  14193  dvdsrvald  14238  dvdsrd  14239  dvdsrtr  14246  unitgrp  14261  rhmopp  14321  aprnzr  14433  lmodfopne  14474  lmodprop2d  14496  lssvacl  14513  lsslss  14529  lss1d  14531  lsspropdg  14579  rnglidlmcl  14628  lidlacl  14632  isridl  14652  znidomb  14806  znunit  14807  znrrg  14808  psrval  14814  mplsubgfilemcl  14854  mplsubgfileminv  14855  mplsubgfi  14856  tgdom  14937  neipsm  15019  tgrest  15034  cnfval  15059  cnpfval  15060  cnpval  15063  iscnp4  15083  cnpnei  15084  cnptopco  15087  cncnpi  15093  cncnp  15095  cnptopresti  15103  cnptoprest2  15105  cndis  15106  lmtopcnp  15115  txbasval  15132  neitx  15133  txcnp  15136  txcnmpt  15138  txcn  15140  imasnopn  15164  psmetres2  15198  isxmet2d  15213  xblss2ps  15269  xblss2  15270  blbas  15298  neibl  15356  metss2lem  15362  metrest  15371  xmettx  15375  metcnp3  15376  metcnp  15377  metcnp2  15378  metcnpi  15380  metcnpi2  15381  mulc1cncf  15454  cncfco  15456  mulcncflem  15472  mulcncf  15473  dedekindeulemuub  15482  dedekindeulemloc  15484  dedekindeulemlu  15486  dedekindeu  15488  suplociccreex  15489  suplociccex  15490  dedekindicclemuub  15491  dedekindicclemloc  15493  dedekindicclemlu  15495  dedekindicclemicc  15497  dedekindicc  15498  ivthinclemlopn  15501  ivthinclemlr  15502  ivthinclemuopn  15503  ivthinclemur  15504  ivthinclemloc  15506  ivthinc  15508  limcimolemlt  15529  limccnp2lem  15541  limccnp2cntop  15542  limccoap  15543  dvcj  15574  dvmptfsum  15590  dveflem  15591  plyf  15602  plyaddlem1  15612  plymullem1  15613  plycolemc  15623  plyco  15624  plycj  15626  dvply1  15630  dvply2g  15631  efltlemlt  15639  sin0pilem1  15646  sin0pilem2  15647  pilem3  15648  coseq0negpitopi  15701  abssinper  15711  cos02pilt1  15716  relogeftb  15730  logbgcd1irraplemexp  15833  logbgcd1irrap  15835  dvdsppwf1o  15857  mpodvdsmulf1o  15858  mersenne  15865  perfectlem2  15868  perfect  15869  lgsval  15877  lgsfvalg  15878  lgsfcl2  15879  lgsval2lem  15883  lgsmod  15899  lgsdilem  15900  lgsdir2lem4  15904  lgsdir2  15906  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem2  15955  2lgslem1a1  15959  2lgslem1a  15961  2sqlem5  15992  2sqlem6  15993  2sqlem7  15994  2sqlem9  15997  2sqlem10  15998  umgrnloopv  16109  uhgr2edg  16201  upgredginwlk  16351  clwwlkccatlem  16395  eupth2lem3lem3fi  16465  eupth2lem3lem4fi  16468  eupth2lemsfi  16473  depindlem3  16503  bj-findis  16749  pwle2  16772  pwf1oexmid  16773  pw1nct  16777  nnsf  16783  peano4nninf  16784  nninfall  16787  nninfsellemeq  16792  nninfsellemeqinf  16794  nnnninfex  16800  nninfnfiinf  16801  qdencn  16807  refeq  16808  trilpolemeq1  16824  trilpolemlt1  16825  trirec0  16828  trimul0or  16845  nconstwlpolemgt0  16850  nconstwlpolem  16851  neapmkvlem  16853  gfsumval  16862  gfsumcl  16870