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  533  simpllr  534  ad5ant123  1241  vtoclgft  2814  reupick  3448  euotd  4288  frirrg  4386  ralxfrd  4498  nnsucpred  4654  foun  5526  f1oprg  5551  dffo4  5713  foeqcnvco  5840  fliftfun  5846  isotr  5866  riotass2  5907  ovmpodxf  6052  mpoxopoveq  6307  tfrlem1  6375  tfrlemibacc  6393  tfrlemibfn  6395  tfrlemi14d  6400  tfrexlem  6401  tfr1onlembacc  6409  tfr1onlembfn  6411  tfr1onlemres  6416  tfrcllembacc  6422  tfrcllembfn  6424  tfrcllemres  6429  frecabcl  6466  nnmordi  6583  eroprf  6696  f1imaen2g  6861  pw2f1odclem  6904  xpen  6915  mapen  6916  mapdom1g  6917  mapxpen  6918  xpmapenlem  6919  phplem4dom  6932  nndomo  6934  phpm  6935  fidifsnen  6940  dif1enen  6950  fisbth  6953  fimax2gtrilemstep  6970  fimax2gtri  6971  en2eqpr  6977  unsnfidcex  6990  unsnfidcel  6991  ssfirab  7006  fidcenumlemrks  7028  sbthlemi8  7039  fiuni  7053  ordiso2  7110  updjud  7157  difinfsnlem  7174  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  enumct  7190  nnnninfeq  7203  nninfisol  7208  enomnilem  7213  fodju0  7222  enmkvlem  7236  enwomnilem  7244  nninfwlpoimlemg  7250  exmidfodomrlemim  7282  exmidontriimlem2  7307  exmidapne  7345  cc3  7353  dfplpq2  7440  nqpi  7464  nqnq0pi  7524  nq0nn  7528  elinp  7560  elnp1st2nd  7562  genprndl  7607  genprndu  7608  addnqprllem  7613  addnqprulem  7614  addnqprl  7615  addnqpru  7616  addlocpr  7622  nqprloc  7631  prmuloc  7652  mulnqprl  7654  mulnqpru  7655  mullocpr  7657  distrlem1prl  7668  distrlem1pru  7669  ltsopr  7682  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemloc  7693  ltexprlemrl  7696  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  aptiprleml  7725  aptiprlemu  7726  archpr  7729  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  archrecpr  7750  caucvgprlemnkj  7752  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemdisj  7760  caucvgprlemloc  7761  caucvgprlemladdfu  7763  caucvgprprlemnkltj  7775  caucvgprprlemnkeqj  7776  caucvgprprlemnjltk  7777  caucvgprprlemml  7780  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemdisj  7788  caucvgprprlemexbt  7792  caucvgprprlemexb  7793  caucvgprprlemaddq  7794  suplocexprlemru  7805  suplocexprlemloc  7807  suplocexprlemex  7808  suplocexprlemub  7809  suplocexprlemlub  7810  mulgt0sr  7864  caucvgsrlemcau  7879  caucvgsrlemoffcau  7884  caucvgsrlemoffres  7886  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  axcaucvglemcau  7984  axcaucvglemres  7985  axpre-suploclemres  7987  axsuploc  8118  cnegexlem1  8220  cnegex  8223  apsym  8652  apcotr  8653  apadd1  8654  mulext1  8658  mulge0  8665  apti  8668  aprcl  8692  conjmulap  8775  lemulge11  8912  creui  9006  nndiv  9050  zaddcllemneg  9384  suprzclex  9443  eluzuzle  9628  infregelbex  9691  divfnzn  9714  qapne  9732  xrltso  9890  xnn0dcle  9896  xnn0letri  9897  xrre  9914  xrre3  9916  xaddf  9938  xaddval  9939  xpncan  9965  xleadd1a  9967  xltadd1  9970  xleaddadd  9981  ixxss12  10000  elioc2  10030  elico2  10031  elicc2  10032  fzm1  10194  fzneuz  10195  eluzgtdifelfzo  10292  elfzonelfzo  10325  exfzdc  10335  zsupcllemstep  10338  infssuzex  10342  suprzubdc  10345  nninfdcex  10346  zsupssdc  10347  qtri3or  10349  exbtwnzlemstep  10356  exbtwnzlemex  10358  exbtwnz  10359  modqid  10460  modqcyc2  10471  modqmuladd  10477  modqmuladdnn0  10479  modaddmodlo  10499  addmodlteq  10509  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdgsuc  10525  frecuzrdgsuctlem  10534  nninfinf  10554  seq3clss  10582  iseqf1olemqcl  10610  iseqf1olemnab  10612  iseqf1olemab  10613  iseqf1olemmo  10616  iseqf1olemqf1o  10617  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  seq3f1olemp  10626  seq3f1oleml  10627  seq3f1o  10628  seqf1oglem1  10630  seqf1oglem2  10631  seqf1og  10632  seq3id3  10635  seqfeq4g  10642  ser3ge0  10647  exp3val  10652  expap0  10680  qsqeqor  10761  modqexp  10777  nn0ltexp2  10820  facndiv  10850  faclbnd  10852  bcval5  10874  hashunlem  10915  hashun  10916  hashprg  10919  fiprsshashgt1  10928  hashfacen  10947  zfz1isolemiso  10950  zfz1isolem1  10951  seq3coll  10953  ovshftex  11003  2shfti  11015  seq3shft  11022  cjap  11090  caucvgrelemcau  11164  cvg1nlemcau  11168  cvg1nlemres  11169  recvguniq  11179  resqrexlemdecn  11196  resqrexlemcalc3  11200  resqrexlemcvg  11203  resqrexlemoverl  11205  leabs  11258  absexpzap  11264  ltabs  11271  abslt  11272  absle  11273  maxleim  11389  maxabslemval  11392  fimaxre2  11411  minmax  11414  2zinfmin  11427  xrmaxiflemcl  11429  xrmaxifle  11430  xrmaxiflemab  11431  xrmaxiflemlub  11432  xrmaxiflemcom  11433  xrmaxltsup  11442  xrmaxadd  11445  xrminmax  11449  xrbdtri  11460  2clim  11485  climshftlemg  11486  climsqz  11519  climsqz2  11520  climrecvg1n  11532  climcvg1nlem  11533  serf0  11536  sumrbdclem  11561  fsum3cvg  11562  summodclem3  11564  summodclem2a  11565  summodclem2  11566  zsumdc  11568  fsum3  11571  isumss  11575  fisumss  11576  fsum3cvg3  11580  fsumcl2lem  11582  fsumadd  11590  fsumsplit  11591  sumsnf  11593  fsum2d  11619  fisum0diag2  11631  fsummulc2  11632  modfsummod  11642  fsumabs  11649  fsumrelem  11655  fsumiun  11661  geoisumr  11702  cvgratnnlemseq  11710  cvgratz  11716  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  prodrbdclem  11755  fproddccvg  11756  prodmodclem3  11759  prodmodclem2a  11760  zproddc  11763  fprodseq  11767  fprodntrivap  11768  fprodssdc  11774  fprodmul  11775  prodsnf  11776  fprodsplitdc  11780  fprodsplit  11781  fprodunsn  11788  fprodcl2lem  11789  fprodap0  11805  fprod2d  11807  fprodrec  11813  fprodap0f  11820  efcj  11857  efaddlem  11858  tanaddaplem  11922  sinltxirr  11945  nndivides  11981  dvdsext  12039  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  bitsfzolem  12138  bitsmod  12140  bitsinv1  12146  dvdsbnd  12150  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlemzz  12196  bezoutlemaz  12197  bezoutlembz  12198  bezoutlemeu  12201  bezoutlemle  12202  bezoutlemsup  12203  dfgcd3  12204  dfgcd2  12208  bezoutr1  12227  nnmindc  12228  nninfctlemfo  12234  dvdslcm  12264  lcmgcdlem  12272  qredeq  12291  qredeu  12292  divgcdcoprm0  12296  divgcdcoprmex  12297  cncongr1  12298  isprm2lem  12311  prmind2  12315  exprmfct  12333  prmdvdsfz  12334  isprm5lem  12336  prmexpb  12346  rpexp1i  12349  sqrt2irr  12357  sqne2sq  12372  nonsq  12402  phiprmpw  12417  eulerthlemrprm  12424  eulerthlema  12425  hashgcdeq  12435  phisum  12436  modprmn0modprm0  12452  pclemub  12483  pclemdc  12484  pcmul  12497  pcqmul  12499  pcxqcl  12508  pcdvdstr  12523  pcprmpw2  12529  difsqpwdvds  12534  pcmpt  12539  oddprmdvds  12550  prmpwdvds  12551  pockthg  12553  infpnlem1  12555  1arith  12563  4sqlem2  12585  4sqlemafi  12591  4sqlemffi  12592  4sqleminfi  12593  4sqlem11  12597  4sqlem13m  12599  4sqlem14  12600  4sqlem17  12603  4sqlem18  12604  ennnfonelemg  12647  ennnfoneleminc  12655  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemfun  12661  ennnfonelemf1  12662  ennnfonelemrn  12663  ennnfonelemdm  12664  ennnfonelemnn0  12666  ennnfonelemim  12668  exmidunben  12670  ctinfomlemom  12671  ctinf  12674  ctiunctlemudc  12681  nninfdclemlt  12695  nninfdclemf1  12696  isstruct2r  12716  prdsval  12977  imasival  13010  gsumpropd2  13097  sgrppropd  13117  prdssgrpd  13119  mndpropd  13144  issubmnd  13146  prdsidlem  13151  prdsmndd  13152  pws0g  13155  mndissubm  13179  resmhm2b  13193  mhmeql  13196  gsumfzz  13199  gsumwsubmcl  13200  gsumwmhm  13202  gsumfzcl  13203  grpinvnz  13275  pwssub  13317  mhmmnd  13324  mulgfng  13332  mulgz  13358  mulgnndir  13359  mulgnn0dir  13360  mulgneg2  13364  mulgass  13367  mhmmulg  13371  issubgrpd2  13398  issubg4m  13401  grpissubg  13402  isnsg3  13415  ghmpreima  13474  ghmnsgpreima  13477  ghmf1  13481  conjnmz  13487  conjnmzb  13488  eqgabl  13538  gsumfzreidx  13545  gsumfzsubmcl  13546  gsumfzmptfidmadd  13547  gsumfzmhm  13551  rngpropd  13589  issrg  13599  ringpropd  13672  ringinvnz1ne0  13683  dvdsrvald  13727  dvdsrd  13728  dvdsrtr  13735  unitgrp  13750  rhmopp  13810  lmodfopne  13960  lmodprop2d  13982  lssvacl  13999  lsslss  14015  lss1d  14017  lsspropdg  14065  rnglidlmcl  14114  lidlacl  14118  isridl  14138  znidomb  14292  znunit  14293  znrrg  14294  psrval  14300  mplsubgfilemcl  14333  mplsubgfileminv  14334  mplsubgfi  14335  tgdom  14416  neipsm  14498  tgrest  14513  cnfval  14538  cnpfval  14539  cnpval  14542  iscnp4  14562  cnpnei  14563  cnptopco  14566  cncnpi  14572  cncnp  14574  cnptopresti  14582  cnptoprest2  14584  cndis  14585  lmtopcnp  14594  txbasval  14611  neitx  14612  txcnp  14615  txcnmpt  14617  txcn  14619  imasnopn  14643  psmetres2  14677  isxmet2d  14692  xblss2ps  14748  xblss2  14749  blbas  14777  neibl  14835  metss2lem  14841  metrest  14850  xmettx  14854  metcnp3  14855  metcnp  14856  metcnp2  14857  metcnpi  14859  metcnpi2  14860  mulc1cncf  14933  cncfco  14935  mulcncflem  14951  mulcncf  14952  dedekindeulemuub  14961  dedekindeulemloc  14963  dedekindeulemlu  14965  dedekindeu  14967  suplociccreex  14968  suplociccex  14969  dedekindicclemuub  14970  dedekindicclemloc  14972  dedekindicclemlu  14974  dedekindicclemicc  14976  dedekindicc  14977  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemloc  14985  ivthinc  14987  limcimolemlt  15008  limccnp2lem  15020  limccnp2cntop  15021  limccoap  15022  dvcj  15053  dvmptfsum  15069  dveflem  15070  plyf  15081  plyaddlem1  15091  plymullem1  15092  plycolemc  15102  plyco  15103  plycj  15105  dvply1  15109  dvply2g  15110  efltlemlt  15118  sin0pilem1  15125  sin0pilem2  15126  pilem3  15127  coseq0negpitopi  15180  abssinper  15190  cos02pilt1  15195  relogeftb  15209  logbgcd1irraplemexp  15312  logbgcd1irrap  15314  dvdsppwf1o  15333  mpodvdsmulf1o  15334  mersenne  15341  perfectlem2  15344  perfect  15345  lgsval  15353  lgsfvalg  15354  lgsfcl2  15355  lgsval2lem  15359  lgsmod  15375  lgsdilem  15376  lgsdir2lem4  15380  lgsdir2  15382  lgsdir  15384  lgsdilem2  15385  lgsdi  15386  lgsne0  15387  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem2  15431  2lgslem1a1  15435  2lgslem1a  15437  2sqlem5  15468  2sqlem6  15469  2sqlem7  15470  2sqlem9  15473  2sqlem10  15474  bj-findis  15733  2omap  15750  pwle2  15753  pwf1oexmid  15754  pw1nct  15758  nnsf  15760  peano4nninf  15761  nninfall  15764  nninfsellemeq  15769  nninfsellemeqinf  15771  nnnninfex  15777  nninfnfiinf  15778  qdencn  15784  refeq  15785  trilpolemeq1  15797  trilpolemlt1  15798  trirec0  15801  nconstwlpolemgt0  15821  nconstwlpolem  15822  neapmkvlem  15824