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  5830  foeqcnvco  5931  fliftfun  5937  isotr  5957  riotass2  6000  ovmpodxf  6147  mpoxopoveq  6406  tfrlem1  6474  tfrlemibacc  6492  tfrlemibfn  6494  tfrlemi14d  6499  tfrexlem  6500  tfr1onlembacc  6508  tfr1onlembfn  6510  tfr1onlemres  6515  tfrcllembacc  6521  tfrcllembfn  6523  tfrcllemres  6528  frecabcl  6565  nnmordi  6684  eroprf  6797  f1imaen2g  6967  pw2f1odclem  7020  xpen  7031  mapen  7032  mapdom1g  7033  mapxpen  7034  xpmapenlem  7035  phplem4dom  7048  nndomo  7050  phpm  7052  fidifsnen  7057  dif1enen  7069  fisbth  7072  fimax2gtrilemstep  7090  fimax2gtri  7091  eqsndc  7095  en2eqpr  7099  unsnfidcex  7112  unsnfidcel  7113  ssfirab  7129  fidcenumlemrks  7152  sbthlemi8  7163  fiuni  7177  ordiso2  7234  updjud  7281  difinfsnlem  7298  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  enumct  7314  nnnninfeq  7327  nninfisol  7332  enomnilem  7337  fodju0  7346  enmkvlem  7360  enwomnilem  7368  nninfwlpoimlemg  7374  pr1or2  7399  pr2cv1  7400  exmidfodomrlemim  7412  exmidontriimlem2  7437  exmidapne  7479  cc3  7487  dfplpq2  7574  nqpi  7598  nqnq0pi  7658  nq0nn  7662  elinp  7694  elnp1st2nd  7696  genprndl  7741  genprndu  7742  addnqprllem  7747  addnqprulem  7748  addnqprl  7749  addnqpru  7750  addlocpr  7756  nqprloc  7765  prmuloc  7786  mulnqprl  7788  mulnqpru  7789  mullocpr  7791  distrlem1prl  7802  distrlem1pru  7803  ltsopr  7816  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  aptiprleml  7859  aptiprlemu  7860  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  archrecpr  7884  caucvgprlemnkj  7886  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnjltk  7911  caucvgprprlemml  7914  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemdisj  7922  caucvgprprlemexbt  7926  caucvgprprlemexb  7927  caucvgprprlemaddq  7928  suplocexprlemru  7939  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  suplocexprlemlub  7944  mulgt0sr  7998  caucvgsrlemcau  8013  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  axsuploc  8252  cnegexlem1  8354  cnegex  8357  apsym  8786  apcotr  8787  apadd1  8788  mulext1  8792  mulge0  8799  apti  8802  aprcl  8826  conjmulap  8909  lemulge11  9046  creui  9140  nndiv  9184  zaddcllemneg  9518  suprzclex  9578  eluzuzle  9764  infregelbex  9832  divfnzn  9855  qapne  9873  xrltso  10031  xnn0dcle  10037  xnn0letri  10038  xrre  10055  xrre3  10057  xaddf  10079  xaddval  10080  xpncan  10106  xleadd1a  10108  xltadd1  10111  xleaddadd  10122  ixxss12  10141  elioc2  10171  elico2  10172  elicc2  10173  fzm1  10335  fzneuz  10336  eluzgtdifelfzo  10443  elfzonelfzo  10476  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  nninfdcex  10498  zsupssdc  10499  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemex  10510  exbtwnz  10511  modqid  10612  modqcyc2  10623  modqmuladd  10629  modqmuladdnn0  10631  modaddmodlo  10651  addmodlteq  10661  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgsuc  10677  frecuzrdgsuctlem  10686  nninfinf  10706  seq3clss  10734  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemmo  10768  iseqf1olemqf1o  10769  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemp  10778  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  seq3id3  10787  seqfeq4g  10794  ser3ge0  10799  exp3val  10804  expap0  10832  qsqeqor  10913  modqexp  10929  nn0ltexp2  10972  facndiv  11002  faclbnd  11004  bcval5  11026  hashunlem  11068  hashun  11069  hashprg  11073  fiprsshashgt1  11082  hashfacen  11101  zfz1isolemiso  11104  zfz1isolem1  11105  seq3coll  11107  hashtpglem  11111  ccatcl  11174  ccatlen  11176  ccatvalfn  11182  ccatsymb  11183  ccatrn  11190  ccat2s1fstg  11229  swrdclg  11235  swrdspsleq  11252  pfxeq  11281  swrdswrd  11290  wrdind  11307  wrd2ind  11308  swrdccatin1  11310  swrdccatin2  11314  pfxccatin12  11318  pfxccat3  11319  swrdccat3b  11325  reuccatpfxs1  11332  ovshftex  11384  2shfti  11396  seq3shft  11403  cjap  11471  caucvgrelemcau  11545  cvg1nlemcau  11549  cvg1nlemres  11550  recvguniq  11560  resqrexlemdecn  11577  resqrexlemcalc3  11581  resqrexlemcvg  11584  resqrexlemoverl  11586  leabs  11639  absexpzap  11645  ltabs  11652  abslt  11653  absle  11654  maxleim  11770  maxabslemval  11773  fimaxre2  11792  minmax  11795  2zinfmin  11808  xrmaxiflemcl  11810  xrmaxifle  11811  xrmaxiflemab  11812  xrmaxiflemlub  11813  xrmaxiflemcom  11814  xrmaxltsup  11823  xrmaxadd  11826  xrminmax  11830  xrbdtri  11841  2clim  11866  climshftlemg  11867  climsqz  11900  climsqz2  11901  climrecvg1n  11913  climcvg1nlem  11914  serf0  11917  sumrbdclem  11943  fsum3cvg  11944  summodclem3  11946  summodclem2a  11947  summodclem2  11948  zsumdc  11950  fsum3  11953  isumss  11957  fisumss  11958  fsum3cvg3  11962  fsumcl2lem  11964  fsumadd  11972  fsumsplit  11973  sumsnf  11975  fsum2d  12001  fisum0diag2  12013  fsummulc2  12014  modfsummod  12024  fsumabs  12031  fsumrelem  12037  fsumiun  12043  geoisumr  12084  cvgratnnlemseq  12092  cvgratz  12098  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  prodrbdclem  12137  fproddccvg  12138  prodmodclem3  12141  prodmodclem2a  12142  zproddc  12145  fprodseq  12149  fprodntrivap  12150  fprodssdc  12156  fprodmul  12157  prodsnf  12158  fprodsplitdc  12162  fprodsplit  12163  fprodunsn  12170  fprodcl2lem  12171  fprodap0  12187  fprod2d  12189  fprodrec  12195  fprodap0f  12202  efcj  12239  efaddlem  12240  tanaddaplem  12304  sinltxirr  12327  nndivides  12363  dvdsext  12421  divalglemeunn  12487  divalglemex  12488  divalglemeuneg  12489  bitsfzolem  12520  bitsmod  12522  bitsinv1  12528  dvdsbnd  12532  bezoutlemnewy  12572  bezoutlemstep  12573  bezoutlemmain  12574  bezoutlemzz  12578  bezoutlemaz  12579  bezoutlembz  12580  bezoutlemeu  12583  bezoutlemle  12584  bezoutlemsup  12585  dfgcd3  12586  dfgcd2  12590  bezoutr1  12609  nnmindc  12610  nninfctlemfo  12616  dvdslcm  12646  lcmgcdlem  12654  qredeq  12673  qredeu  12674  divgcdcoprm0  12678  divgcdcoprmex  12679  cncongr1  12680  isprm2lem  12693  prmind2  12697  exprmfct  12715  prmdvdsfz  12716  isprm5lem  12718  prmexpb  12728  rpexp1i  12731  sqrt2irr  12739  sqne2sq  12754  nonsq  12784  phiprmpw  12799  eulerthlemrprm  12806  eulerthlema  12807  hashgcdeq  12817  phisum  12818  modprmn0modprm0  12834  pclemub  12865  pclemdc  12866  pcmul  12879  pcqmul  12881  pcxqcl  12890  pcdvdstr  12905  pcprmpw2  12911  difsqpwdvds  12916  pcmpt  12921  oddprmdvds  12932  prmpwdvds  12933  pockthg  12935  infpnlem1  12937  1arith  12945  4sqlem2  12967  4sqlemafi  12973  4sqlemffi  12974  4sqleminfi  12975  4sqlem11  12979  4sqlem13m  12981  4sqlem14  12982  4sqlem17  12985  4sqlem18  12986  ennnfonelemg  13029  ennnfoneleminc  13037  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ennnfonelemex  13040  ennnfonelemhom  13041  ennnfonelemfun  13043  ennnfonelemf1  13044  ennnfonelemrn  13045  ennnfonelemdm  13046  ennnfonelemnn0  13048  ennnfonelemim  13050  exmidunben  13052  ctinfomlemom  13053  ctinf  13056  ctiunctlemudc  13063  nninfdclemlt  13077  nninfdclemf1  13078  isstruct2r  13098  prdsval  13361  imasival  13394  gsumpropd2  13481  sgrppropd  13501  prdssgrpd  13503  mndpropd  13528  issubmnd  13530  prdsidlem  13535  prdsmndd  13536  pws0g  13539  mndissubm  13563  resmhm2b  13577  mhmeql  13580  gsumfzz  13583  gsumwsubmcl  13584  gsumwmhm  13586  gsumfzcl  13587  grpinvnz  13659  pwssub  13701  mhmmnd  13708  mulgfng  13716  mulgz  13742  mulgnndir  13743  mulgnn0dir  13744  mulgneg2  13748  mulgass  13751  mhmmulg  13755  issubgrpd2  13782  issubg4m  13785  grpissubg  13786  isnsg3  13799  ghmpreima  13858  ghmnsgpreima  13861  ghmf1  13865  conjnmz  13871  conjnmzb  13872  eqgabl  13922  gsumfzreidx  13929  gsumfzsubmcl  13930  gsumfzmptfidmadd  13931  gsumfzmhm  13935  rngpropd  13974  issrg  13984  ringpropd  14057  ringinvnz1ne0  14068  dvdsrvald  14113  dvdsrd  14114  dvdsrtr  14121  unitgrp  14136  rhmopp  14196  lmodfopne  14346  lmodprop2d  14368  lssvacl  14385  lsslss  14401  lss1d  14403  lsspropdg  14451  rnglidlmcl  14500  lidlacl  14504  isridl  14524  znidomb  14678  znunit  14679  znrrg  14680  psrval  14686  mplsubgfilemcl  14719  mplsubgfileminv  14720  mplsubgfi  14721  tgdom  14802  neipsm  14884  tgrest  14899  cnfval  14924  cnpfval  14925  cnpval  14928  iscnp4  14948  cnpnei  14949  cnptopco  14952  cncnpi  14958  cncnp  14960  cnptopresti  14968  cnptoprest2  14970  cndis  14971  lmtopcnp  14980  txbasval  14997  neitx  14998  txcnp  15001  txcnmpt  15003  txcn  15005  imasnopn  15029  psmetres2  15063  isxmet2d  15078  xblss2ps  15134  xblss2  15135  blbas  15163  neibl  15221  metss2lem  15227  metrest  15236  xmettx  15240  metcnp3  15241  metcnp  15242  metcnp2  15243  metcnpi  15245  metcnpi2  15246  mulc1cncf  15319  cncfco  15321  mulcncflem  15337  mulcncf  15338  dedekindeulemuub  15347  dedekindeulemloc  15349  dedekindeulemlu  15351  dedekindeu  15353  suplociccreex  15354  suplociccex  15355  dedekindicclemuub  15356  dedekindicclemloc  15358  dedekindicclemlu  15360  dedekindicclemicc  15362  dedekindicc  15363  ivthinclemlopn  15366  ivthinclemlr  15367  ivthinclemuopn  15368  ivthinclemur  15369  ivthinclemloc  15371  ivthinc  15373  limcimolemlt  15394  limccnp2lem  15406  limccnp2cntop  15407  limccoap  15408  dvcj  15439  dvmptfsum  15455  dveflem  15456  plyf  15467  plyaddlem1  15477  plymullem1  15478  plycolemc  15488  plyco  15489  plycj  15491  dvply1  15495  dvply2g  15496  efltlemlt  15504  sin0pilem1  15511  sin0pilem2  15512  pilem3  15513  coseq0negpitopi  15566  abssinper  15576  cos02pilt1  15581  relogeftb  15595  logbgcd1irraplemexp  15698  logbgcd1irrap  15700  dvdsppwf1o  15719  mpodvdsmulf1o  15720  mersenne  15727  perfectlem2  15730  perfect  15731  lgsval  15739  lgsfvalg  15740  lgsfcl2  15741  lgsval2lem  15745  lgsmod  15761  lgsdilem  15762  lgsdir2lem4  15766  lgsdir2  15768  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  lgsdirnn0  15782  lgsdinn0  15783  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem2  15817  2lgslem1a1  15821  2lgslem1a  15823  2sqlem5  15854  2sqlem6  15855  2sqlem7  15856  2sqlem9  15859  2sqlem10  15860  umgrnloopv  15971  uhgr2edg  16063  upgredginwlk  16213  clwwlkccatlem  16257  eupth2lem3lem3fi  16327  eupth2lem3lem4fi  16330  eupth2lemsfi  16335  depindlem3  16353  bj-findis  16600  2omap  16620  pwle2  16625  pwf1oexmid  16626  pw1nct  16630  nnsf  16633  peano4nninf  16634  nninfall  16637  nninfsellemeq  16642  nninfsellemeqinf  16644  nnnninfex  16650  nninfnfiinf  16651  qdencn  16657  refeq  16658  trilpolemeq1  16670  trilpolemlt1  16671  trirec0  16674  nconstwlpolemgt0  16695  nconstwlpolem  16696  neapmkvlem  16698  gfsumval  16707  gfsumcl  16714