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  1265  vtoclgft  2854  reupick  3491  euotd  4347  frirrg  4447  ralxfrd  4559  nnsucpred  4715  foun  5602  f1oprg  5629  dffo4  5795  funopsn  5829  foeqcnvco  5930  fliftfun  5936  isotr  5956  riotass2  5999  ovmpodxf  6146  mpoxopoveq  6405  tfrlem1  6473  tfrlemibacc  6491  tfrlemibfn  6493  tfrlemi14d  6498  tfrexlem  6499  tfr1onlembacc  6507  tfr1onlembfn  6509  tfr1onlemres  6514  tfrcllembacc  6520  tfrcllembfn  6522  tfrcllemres  6527  frecabcl  6564  nnmordi  6683  eroprf  6796  f1imaen2g  6966  pw2f1odclem  7019  xpen  7030  mapen  7031  mapdom1g  7032  mapxpen  7033  xpmapenlem  7034  phplem4dom  7047  nndomo  7049  phpm  7051  fidifsnen  7056  dif1enen  7068  fisbth  7071  fimax2gtrilemstep  7089  fimax2gtri  7090  eqsndc  7094  en2eqpr  7098  unsnfidcex  7111  unsnfidcel  7112  ssfirab  7128  fidcenumlemrks  7151  sbthlemi8  7162  fiuni  7176  ordiso2  7233  updjud  7280  difinfsnlem  7297  ctssdclemn0  7308  ctssdccl  7309  ctssdc  7311  enumctlemm  7312  enumct  7313  nnnninfeq  7326  nninfisol  7331  enomnilem  7336  fodju0  7345  enmkvlem  7359  enwomnilem  7367  nninfwlpoimlemg  7373  pr1or2  7398  pr2cv1  7399  exmidfodomrlemim  7411  exmidontriimlem2  7436  exmidapne  7478  cc3  7486  dfplpq2  7573  nqpi  7597  nqnq0pi  7657  nq0nn  7661  elinp  7693  elnp1st2nd  7695  genprndl  7740  genprndu  7741  addnqprllem  7746  addnqprulem  7747  addnqprl  7748  addnqpru  7749  addlocpr  7755  nqprloc  7764  prmuloc  7785  mulnqprl  7787  mulnqpru  7788  mullocpr  7790  distrlem1prl  7801  distrlem1pru  7802  ltsopr  7815  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemloc  7826  ltexprlemrl  7829  ltexprlemru  7831  addcanprleml  7833  addcanprlemu  7834  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  aptiprleml  7858  aptiprlemu  7859  archpr  7862  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdru  7875  archrecpr  7883  caucvgprlemnkj  7885  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprprlemnkltj  7908  caucvgprprlemnkeqj  7909  caucvgprprlemnjltk  7910  caucvgprprlemml  7913  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemdisj  7921  caucvgprprlemexbt  7925  caucvgprprlemexb  7926  caucvgprprlemaddq  7927  suplocexprlemru  7938  suplocexprlemloc  7940  suplocexprlemex  7941  suplocexprlemub  7942  suplocexprlemlub  7943  mulgt0sr  7997  caucvgsrlemcau  8012  caucvgsrlemoffcau  8017  caucvgsrlemoffres  8019  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  axcaucvglemcau  8117  axcaucvglemres  8118  axpre-suploclemres  8120  axsuploc  8251  cnegexlem1  8353  cnegex  8356  apsym  8785  apcotr  8786  apadd1  8787  mulext1  8791  mulge0  8798  apti  8801  aprcl  8825  conjmulap  8908  lemulge11  9045  creui  9139  nndiv  9183  zaddcllemneg  9517  suprzclex  9577  eluzuzle  9763  infregelbex  9831  divfnzn  9854  qapne  9872  xrltso  10030  xnn0dcle  10036  xnn0letri  10037  xrre  10054  xrre3  10056  xaddf  10078  xaddval  10079  xpncan  10105  xleadd1a  10107  xltadd1  10110  xleaddadd  10121  ixxss12  10140  elioc2  10170  elico2  10171  elicc2  10172  fzm1  10334  fzneuz  10335  eluzgtdifelfzo  10441  elfzonelfzo  10474  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  suprzubdc  10495  nninfdcex  10496  zsupssdc  10497  qtri3or  10499  exbtwnzlemstep  10506  exbtwnzlemex  10508  exbtwnz  10509  modqid  10610  modqcyc2  10621  modqmuladd  10627  modqmuladdnn0  10629  modaddmodlo  10649  addmodlteq  10659  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgsuc  10675  frecuzrdgsuctlem  10684  nninfinf  10704  seq3clss  10732  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemab  10763  iseqf1olemmo  10766  iseqf1olemqf1o  10767  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seq3f1olemp  10776  seq3f1oleml  10777  seq3f1o  10778  seqf1oglem1  10780  seqf1oglem2  10781  seqf1og  10782  seq3id3  10785  seqfeq4g  10792  ser3ge0  10797  exp3val  10802  expap0  10830  qsqeqor  10911  modqexp  10927  nn0ltexp2  10970  facndiv  11000  faclbnd  11002  bcval5  11024  hashunlem  11066  hashun  11067  hashprg  11071  fiprsshashgt1  11080  hashfacen  11099  zfz1isolemiso  11102  zfz1isolem1  11103  seq3coll  11105  ccatcl  11169  ccatlen  11171  ccatvalfn  11177  ccatsymb  11178  ccatrn  11185  ccat2s1fstg  11224  swrdclg  11230  swrdspsleq  11247  pfxeq  11276  swrdswrd  11285  wrdind  11302  wrd2ind  11303  swrdccatin1  11305  swrdccatin2  11309  pfxccatin12  11313  pfxccat3  11314  swrdccat3b  11320  reuccatpfxs1  11327  ovshftex  11379  2shfti  11391  seq3shft  11398  cjap  11466  caucvgrelemcau  11540  cvg1nlemcau  11544  cvg1nlemres  11545  recvguniq  11555  resqrexlemdecn  11572  resqrexlemcalc3  11576  resqrexlemcvg  11579  resqrexlemoverl  11581  leabs  11634  absexpzap  11640  ltabs  11647  abslt  11648  absle  11649  maxleim  11765  maxabslemval  11768  fimaxre2  11787  minmax  11790  2zinfmin  11803  xrmaxiflemcl  11805  xrmaxifle  11806  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxiflemcom  11809  xrmaxltsup  11818  xrmaxadd  11821  xrminmax  11825  xrbdtri  11836  2clim  11861  climshftlemg  11862  climsqz  11895  climsqz2  11896  climrecvg1n  11908  climcvg1nlem  11909  serf0  11912  sumrbdclem  11937  fsum3cvg  11938  summodclem3  11940  summodclem2a  11941  summodclem2  11942  zsumdc  11944  fsum3  11947  isumss  11951  fisumss  11952  fsum3cvg3  11956  fsumcl2lem  11958  fsumadd  11966  fsumsplit  11967  sumsnf  11969  fsum2d  11995  fisum0diag2  12007  fsummulc2  12008  modfsummod  12018  fsumabs  12025  fsumrelem  12031  fsumiun  12037  geoisumr  12078  cvgratnnlemseq  12086  cvgratz  12092  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  prodrbdclem  12131  fproddccvg  12132  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  fprodntrivap  12144  fprodssdc  12150  fprodmul  12151  prodsnf  12152  fprodsplitdc  12156  fprodsplit  12157  fprodunsn  12164  fprodcl2lem  12165  fprodap0  12181  fprod2d  12183  fprodrec  12189  fprodap0f  12196  efcj  12233  efaddlem  12234  tanaddaplem  12298  sinltxirr  12321  nndivides  12357  dvdsext  12415  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  bitsfzolem  12514  bitsmod  12516  bitsinv1  12522  dvdsbnd  12526  bezoutlemnewy  12566  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlemzz  12572  bezoutlemaz  12573  bezoutlembz  12574  bezoutlemeu  12577  bezoutlemle  12578  bezoutlemsup  12579  dfgcd3  12580  dfgcd2  12584  bezoutr1  12603  nnmindc  12604  nninfctlemfo  12610  dvdslcm  12640  lcmgcdlem  12648  qredeq  12667  qredeu  12668  divgcdcoprm0  12672  divgcdcoprmex  12673  cncongr1  12674  isprm2lem  12687  prmind2  12691  exprmfct  12709  prmdvdsfz  12710  isprm5lem  12712  prmexpb  12722  rpexp1i  12725  sqrt2irr  12733  sqne2sq  12748  nonsq  12778  phiprmpw  12793  eulerthlemrprm  12800  eulerthlema  12801  hashgcdeq  12811  phisum  12812  modprmn0modprm0  12828  pclemub  12859  pclemdc  12860  pcmul  12873  pcqmul  12875  pcxqcl  12884  pcdvdstr  12899  pcprmpw2  12905  difsqpwdvds  12910  pcmpt  12915  oddprmdvds  12926  prmpwdvds  12927  pockthg  12929  infpnlem1  12931  1arith  12939  4sqlem2  12961  4sqlemafi  12967  4sqlemffi  12968  4sqleminfi  12969  4sqlem11  12973  4sqlem13m  12975  4sqlem14  12976  4sqlem17  12979  4sqlem18  12980  ennnfonelemg  13023  ennnfoneleminc  13031  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemfun  13037  ennnfonelemf1  13038  ennnfonelemrn  13039  ennnfonelemdm  13040  ennnfonelemnn0  13042  ennnfonelemim  13044  exmidunben  13046  ctinfomlemom  13047  ctinf  13050  ctiunctlemudc  13057  nninfdclemlt  13071  nninfdclemf1  13072  isstruct2r  13092  prdsval  13355  imasival  13388  gsumpropd2  13475  sgrppropd  13495  prdssgrpd  13497  mndpropd  13522  issubmnd  13524  prdsidlem  13529  prdsmndd  13530  pws0g  13533  mndissubm  13557  resmhm2b  13571  mhmeql  13574  gsumfzz  13577  gsumwsubmcl  13578  gsumwmhm  13580  gsumfzcl  13581  grpinvnz  13653  pwssub  13695  mhmmnd  13702  mulgfng  13710  mulgz  13736  mulgnndir  13737  mulgnn0dir  13738  mulgneg2  13742  mulgass  13745  mhmmulg  13749  issubgrpd2  13776  issubg4m  13779  grpissubg  13780  isnsg3  13793  ghmpreima  13852  ghmnsgpreima  13855  ghmf1  13859  conjnmz  13865  conjnmzb  13866  eqgabl  13916  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  rngpropd  13967  issrg  13977  ringpropd  14050  ringinvnz1ne0  14061  dvdsrvald  14106  dvdsrd  14107  dvdsrtr  14114  unitgrp  14129  rhmopp  14189  lmodfopne  14339  lmodprop2d  14361  lssvacl  14378  lsslss  14394  lss1d  14396  lsspropdg  14444  rnglidlmcl  14493  lidlacl  14497  isridl  14517  znidomb  14671  znunit  14672  znrrg  14673  psrval  14679  mplsubgfilemcl  14712  mplsubgfileminv  14713  mplsubgfi  14714  tgdom  14795  neipsm  14877  tgrest  14892  cnfval  14917  cnpfval  14918  cnpval  14921  iscnp4  14941  cnpnei  14942  cnptopco  14945  cncnpi  14951  cncnp  14953  cnptopresti  14961  cnptoprest2  14963  cndis  14964  lmtopcnp  14973  txbasval  14990  neitx  14991  txcnp  14994  txcnmpt  14996  txcn  14998  imasnopn  15022  psmetres2  15056  isxmet2d  15071  xblss2ps  15127  xblss2  15128  blbas  15156  neibl  15214  metss2lem  15220  metrest  15229  xmettx  15233  metcnp3  15234  metcnp  15235  metcnp2  15236  metcnpi  15238  metcnpi2  15239  mulc1cncf  15312  cncfco  15314  mulcncflem  15330  mulcncf  15331  dedekindeulemuub  15340  dedekindeulemloc  15342  dedekindeulemlu  15344  dedekindeu  15346  suplociccreex  15347  suplociccex  15348  dedekindicclemuub  15349  dedekindicclemloc  15351  dedekindicclemlu  15353  dedekindicclemicc  15355  dedekindicc  15356  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemloc  15364  ivthinc  15366  limcimolemlt  15387  limccnp2lem  15399  limccnp2cntop  15400  limccoap  15401  dvcj  15432  dvmptfsum  15448  dveflem  15449  plyf  15460  plyaddlem1  15470  plymullem1  15471  plycolemc  15481  plyco  15482  plycj  15484  dvply1  15488  dvply2g  15489  efltlemlt  15497  sin0pilem1  15504  sin0pilem2  15505  pilem3  15506  coseq0negpitopi  15559  abssinper  15569  cos02pilt1  15574  relogeftb  15588  logbgcd1irraplemexp  15691  logbgcd1irrap  15693  dvdsppwf1o  15712  mpodvdsmulf1o  15713  mersenne  15720  perfectlem2  15723  perfect  15724  lgsval  15732  lgsfvalg  15733  lgsfcl2  15734  lgsval2lem  15738  lgsmod  15754  lgsdilem  15755  lgsdir2lem4  15759  lgsdir2  15761  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem2  15810  2lgslem1a1  15814  2lgslem1a  15816  2sqlem5  15847  2sqlem6  15848  2sqlem7  15849  2sqlem9  15852  2sqlem10  15853  umgrnloopv  15964  uhgr2edg  16056  upgredginwlk  16206  clwwlkccatlem  16250  bj-findis  16574  2omap  16594  pwle2  16599  pwf1oexmid  16600  pw1nct  16604  nnsf  16607  peano4nninf  16608  nninfall  16611  nninfsellemeq  16616  nninfsellemeqinf  16618  nnnninfex  16624  nninfnfiinf  16625  qdencn  16631  refeq  16632  trilpolemeq1  16644  trilpolemlt1  16645  trirec0  16648  nconstwlpolemgt0  16668  nconstwlpolem  16669  neapmkvlem  16671  gfsumval  16680