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  1263  vtoclgft  2851  reupick  3488  euotd  4341  frirrg  4441  ralxfrd  4553  nnsucpred  4709  foun  5593  f1oprg  5619  dffo4  5785  funopsn  5819  foeqcnvco  5920  fliftfun  5926  isotr  5946  riotass2  5989  ovmpodxf  6136  mpoxopoveq  6392  tfrlem1  6460  tfrlemibacc  6478  tfrlemibfn  6480  tfrlemi14d  6485  tfrexlem  6486  tfr1onlembacc  6494  tfr1onlembfn  6496  tfr1onlemres  6501  tfrcllembacc  6507  tfrcllembfn  6509  tfrcllemres  6514  frecabcl  6551  nnmordi  6670  eroprf  6783  f1imaen2g  6953  pw2f1odclem  7003  xpen  7014  mapen  7015  mapdom1g  7016  mapxpen  7017  xpmapenlem  7018  phplem4dom  7031  nndomo  7033  phpm  7035  fidifsnen  7040  dif1enen  7050  fisbth  7053  fimax2gtrilemstep  7071  fimax2gtri  7072  eqsndc  7076  en2eqpr  7080  unsnfidcex  7093  unsnfidcel  7094  ssfirab  7109  fidcenumlemrks  7131  sbthlemi8  7142  fiuni  7156  ordiso2  7213  updjud  7260  difinfsnlem  7277  ctssdclemn0  7288  ctssdccl  7289  ctssdc  7291  enumctlemm  7292  enumct  7293  nnnninfeq  7306  nninfisol  7311  enomnilem  7316  fodju0  7325  enmkvlem  7339  enwomnilem  7347  nninfwlpoimlemg  7353  pr1or2  7378  pr2cv1  7379  exmidfodomrlemim  7390  exmidontriimlem2  7415  exmidapne  7457  cc3  7465  dfplpq2  7552  nqpi  7576  nqnq0pi  7636  nq0nn  7640  elinp  7672  elnp1st2nd  7674  genprndl  7719  genprndu  7720  addnqprllem  7725  addnqprulem  7726  addnqprl  7727  addnqpru  7728  addlocpr  7734  nqprloc  7743  prmuloc  7764  mulnqprl  7766  mulnqpru  7767  mullocpr  7769  distrlem1prl  7780  distrlem1pru  7781  ltsopr  7794  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  aptiprleml  7837  aptiprlemu  7838  archpr  7841  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  archrecpr  7862  caucvgprlemnkj  7864  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnjltk  7889  caucvgprprlemml  7892  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemdisj  7900  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  caucvgprprlemaddq  7906  suplocexprlemru  7917  suplocexprlemloc  7919  suplocexprlemex  7920  suplocexprlemub  7921  suplocexprlemlub  7922  mulgt0sr  7976  caucvgsrlemcau  7991  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  axsuploc  8230  cnegexlem1  8332  cnegex  8335  apsym  8764  apcotr  8765  apadd1  8766  mulext1  8770  mulge0  8777  apti  8780  aprcl  8804  conjmulap  8887  lemulge11  9024  creui  9118  nndiv  9162  zaddcllemneg  9496  suprzclex  9556  eluzuzle  9742  infregelbex  9805  divfnzn  9828  qapne  9846  xrltso  10004  xnn0dcle  10010  xnn0letri  10011  xrre  10028  xrre3  10030  xaddf  10052  xaddval  10053  xpncan  10079  xleadd1a  10081  xltadd1  10084  xleaddadd  10095  ixxss12  10114  elioc2  10144  elico2  10145  elicc2  10146  fzm1  10308  fzneuz  10309  eluzgtdifelfzo  10415  elfzonelfzo  10448  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  suprzubdc  10468  nninfdcex  10469  zsupssdc  10470  qtri3or  10472  exbtwnzlemstep  10479  exbtwnzlemex  10481  exbtwnz  10482  modqid  10583  modqcyc2  10594  modqmuladd  10600  modqmuladdnn0  10602  modaddmodlo  10622  addmodlteq  10632  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgsuc  10648  frecuzrdgsuctlem  10657  nninfinf  10677  seq3clss  10705  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemab  10736  iseqf1olemmo  10739  iseqf1olemqf1o  10740  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1olemp  10749  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem1  10753  seqf1oglem2  10754  seqf1og  10755  seq3id3  10758  seqfeq4g  10765  ser3ge0  10770  exp3val  10775  expap0  10803  qsqeqor  10884  modqexp  10900  nn0ltexp2  10943  facndiv  10973  faclbnd  10975  bcval5  10997  hashunlem  11038  hashun  11039  hashprg  11043  fiprsshashgt1  11052  hashfacen  11071  zfz1isolemiso  11074  zfz1isolem1  11075  seq3coll  11077  ccatcl  11141  ccatlen  11143  ccatvalfn  11149  ccatsymb  11150  ccatrn  11157  swrdclg  11197  swrdspsleq  11214  pfxeq  11243  swrdswrd  11252  wrdind  11269  wrd2ind  11270  swrdccatin1  11272  swrdccatin2  11276  pfxccatin12  11280  pfxccat3  11281  swrdccat3b  11287  reuccatpfxs1  11294  ovshftex  11345  2shfti  11357  seq3shft  11364  cjap  11432  caucvgrelemcau  11506  cvg1nlemcau  11510  cvg1nlemres  11511  recvguniq  11521  resqrexlemdecn  11538  resqrexlemcalc3  11542  resqrexlemcvg  11545  resqrexlemoverl  11547  leabs  11600  absexpzap  11606  ltabs  11613  abslt  11614  absle  11615  maxleim  11731  maxabslemval  11734  fimaxre2  11753  minmax  11756  2zinfmin  11769  xrmaxiflemcl  11771  xrmaxifle  11772  xrmaxiflemab  11773  xrmaxiflemlub  11774  xrmaxiflemcom  11775  xrmaxltsup  11784  xrmaxadd  11787  xrminmax  11791  xrbdtri  11802  2clim  11827  climshftlemg  11828  climsqz  11861  climsqz2  11862  climrecvg1n  11874  climcvg1nlem  11875  serf0  11878  sumrbdclem  11903  fsum3cvg  11904  summodclem3  11906  summodclem2a  11907  summodclem2  11908  zsumdc  11910  fsum3  11913  isumss  11917  fisumss  11918  fsum3cvg3  11922  fsumcl2lem  11924  fsumadd  11932  fsumsplit  11933  sumsnf  11935  fsum2d  11961  fisum0diag2  11973  fsummulc2  11974  modfsummod  11984  fsumabs  11991  fsumrelem  11997  fsumiun  12003  geoisumr  12044  cvgratnnlemseq  12052  cvgratz  12058  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  prodrbdclem  12097  fproddccvg  12098  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  fprodntrivap  12110  fprodssdc  12116  fprodmul  12117  prodsnf  12118  fprodsplitdc  12122  fprodsplit  12123  fprodunsn  12130  fprodcl2lem  12131  fprodap0  12147  fprod2d  12149  fprodrec  12155  fprodap0f  12162  efcj  12199  efaddlem  12200  tanaddaplem  12264  sinltxirr  12287  nndivides  12323  dvdsext  12381  divalglemeunn  12447  divalglemex  12448  divalglemeuneg  12449  bitsfzolem  12480  bitsmod  12482  bitsinv1  12488  dvdsbnd  12492  bezoutlemnewy  12532  bezoutlemstep  12533  bezoutlemmain  12534  bezoutlemzz  12538  bezoutlemaz  12539  bezoutlembz  12540  bezoutlemeu  12543  bezoutlemle  12544  bezoutlemsup  12545  dfgcd3  12546  dfgcd2  12550  bezoutr1  12569  nnmindc  12570  nninfctlemfo  12576  dvdslcm  12606  lcmgcdlem  12614  qredeq  12633  qredeu  12634  divgcdcoprm0  12638  divgcdcoprmex  12639  cncongr1  12640  isprm2lem  12653  prmind2  12657  exprmfct  12675  prmdvdsfz  12676  isprm5lem  12678  prmexpb  12688  rpexp1i  12691  sqrt2irr  12699  sqne2sq  12714  nonsq  12744  phiprmpw  12759  eulerthlemrprm  12766  eulerthlema  12767  hashgcdeq  12777  phisum  12778  modprmn0modprm0  12794  pclemub  12825  pclemdc  12826  pcmul  12839  pcqmul  12841  pcxqcl  12850  pcdvdstr  12865  pcprmpw2  12871  difsqpwdvds  12876  pcmpt  12881  oddprmdvds  12892  prmpwdvds  12893  pockthg  12895  infpnlem1  12897  1arith  12905  4sqlem2  12927  4sqlemafi  12933  4sqlemffi  12934  4sqleminfi  12935  4sqlem11  12939  4sqlem13m  12941  4sqlem14  12942  4sqlem17  12945  4sqlem18  12946  ennnfonelemg  12989  ennnfoneleminc  12997  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemex  13000  ennnfonelemhom  13001  ennnfonelemfun  13003  ennnfonelemf1  13004  ennnfonelemrn  13005  ennnfonelemdm  13006  ennnfonelemnn0  13008  ennnfonelemim  13010  exmidunben  13012  ctinfomlemom  13013  ctinf  13016  ctiunctlemudc  13023  nninfdclemlt  13037  nninfdclemf1  13038  isstruct2r  13058  prdsval  13321  imasival  13354  gsumpropd2  13441  sgrppropd  13461  prdssgrpd  13463  mndpropd  13488  issubmnd  13490  prdsidlem  13495  prdsmndd  13496  pws0g  13499  mndissubm  13523  resmhm2b  13537  mhmeql  13540  gsumfzz  13543  gsumwsubmcl  13544  gsumwmhm  13546  gsumfzcl  13547  grpinvnz  13619  pwssub  13661  mhmmnd  13668  mulgfng  13676  mulgz  13702  mulgnndir  13703  mulgnn0dir  13704  mulgneg2  13708  mulgass  13711  mhmmulg  13715  issubgrpd2  13742  issubg4m  13745  grpissubg  13746  isnsg3  13759  ghmpreima  13818  ghmnsgpreima  13821  ghmf1  13825  conjnmz  13831  conjnmzb  13832  eqgabl  13882  gsumfzreidx  13889  gsumfzsubmcl  13890  gsumfzmptfidmadd  13891  gsumfzmhm  13895  rngpropd  13933  issrg  13943  ringpropd  14016  ringinvnz1ne0  14027  dvdsrvald  14072  dvdsrd  14073  dvdsrtr  14080  unitgrp  14095  rhmopp  14155  lmodfopne  14305  lmodprop2d  14327  lssvacl  14344  lsslss  14360  lss1d  14362  lsspropdg  14410  rnglidlmcl  14459  lidlacl  14463  isridl  14483  znidomb  14637  znunit  14638  znrrg  14639  psrval  14645  mplsubgfilemcl  14678  mplsubgfileminv  14679  mplsubgfi  14680  tgdom  14761  neipsm  14843  tgrest  14858  cnfval  14883  cnpfval  14884  cnpval  14887  iscnp4  14907  cnpnei  14908  cnptopco  14911  cncnpi  14917  cncnp  14919  cnptopresti  14927  cnptoprest2  14929  cndis  14930  lmtopcnp  14939  txbasval  14956  neitx  14957  txcnp  14960  txcnmpt  14962  txcn  14964  imasnopn  14988  psmetres2  15022  isxmet2d  15037  xblss2ps  15093  xblss2  15094  blbas  15122  neibl  15180  metss2lem  15186  metrest  15195  xmettx  15199  metcnp3  15200  metcnp  15201  metcnp2  15202  metcnpi  15204  metcnpi2  15205  mulc1cncf  15278  cncfco  15280  mulcncflem  15296  mulcncf  15297  dedekindeulemuub  15306  dedekindeulemloc  15308  dedekindeulemlu  15310  dedekindeu  15312  suplociccreex  15313  suplociccex  15314  dedekindicclemuub  15315  dedekindicclemloc  15317  dedekindicclemlu  15319  dedekindicclemicc  15321  dedekindicc  15322  ivthinclemlopn  15325  ivthinclemlr  15326  ivthinclemuopn  15327  ivthinclemur  15328  ivthinclemloc  15330  ivthinc  15332  limcimolemlt  15353  limccnp2lem  15365  limccnp2cntop  15366  limccoap  15367  dvcj  15398  dvmptfsum  15414  dveflem  15415  plyf  15426  plyaddlem1  15436  plymullem1  15437  plycolemc  15447  plyco  15448  plycj  15450  dvply1  15454  dvply2g  15455  efltlemlt  15463  sin0pilem1  15470  sin0pilem2  15471  pilem3  15472  coseq0negpitopi  15525  abssinper  15535  cos02pilt1  15540  relogeftb  15554  logbgcd1irraplemexp  15657  logbgcd1irrap  15659  dvdsppwf1o  15678  mpodvdsmulf1o  15679  mersenne  15686  perfectlem2  15689  perfect  15690  lgsval  15698  lgsfvalg  15699  lgsfcl2  15700  lgsval2lem  15704  lgsmod  15720  lgsdilem  15721  lgsdir2lem4  15725  lgsdir2  15727  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  lgsdirnn0  15741  lgsdinn0  15742  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem2  15776  2lgslem1a1  15780  2lgslem1a  15782  2sqlem5  15813  2sqlem6  15814  2sqlem7  15815  2sqlem9  15818  2sqlem10  15819  umgrnloopv  15929  uhgr2edg  16019  upgredginwlk  16097  clwwlkccatlem  16137  bj-findis  16397  2omap  16418  pwle2  16423  pwf1oexmid  16424  pw1nct  16428  nnsf  16431  peano4nninf  16432  nninfall  16435  nninfsellemeq  16440  nninfsellemeqinf  16442  nnnninfex  16448  nninfnfiinf  16449  qdencn  16455  refeq  16456  trilpolemeq1  16468  trilpolemlt1  16469  trirec0  16472  nconstwlpolemgt0  16492  nconstwlpolem  16493  neapmkvlem  16495