Theorem ad2antrr 480

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 274	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantlr 469	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  ad3antrrr  484  ad5ant13  511  ad5ant23  514  simpll  519  simplll  523  simpllr  524  vtoclgft  2775  reupick  3405  euotd  4231  frirrg  4327  ralxfrd  4439  nnsucpred  4593  foun  5450  f1oprg  5475  dffo4  5632  foeqcnvco  5757  fliftfun  5763  isotr  5783  riotass2  5823  ovmpodxf  5963  mpoxopoveq  6204  tfrlem1  6272  tfrlemibacc  6290  tfrlemibfn  6292  tfrlemi14d  6297  tfrexlem  6298  tfr1onlembacc  6306  tfr1onlembfn  6308  tfr1onlemres  6313  tfrcllembacc  6319  tfrcllembfn  6321  tfrcllemres  6326  frecabcl  6363  nnmordi  6480  eroprf  6590  f1imaen2g  6755  xpen  6807  mapen  6808  mapdom1g  6809  mapxpen  6810  xpmapenlem  6811  phplem4dom  6824  nndomo  6826  phpm  6827  fidifsnen  6832  dif1enen  6842  fisbth  6845  fimax2gtrilemstep  6862  fimax2gtri  6863  en2eqpr  6869  unsnfidcex  6881  unsnfidcel  6882  ssfirab  6895  fidcenumlemrks  6914  sbthlemi8  6925  fiuni  6939  ordiso2  6996  updjud  7043  difinfsnlem  7060  ctssdclemn0  7071  ctssdccl  7072  ctssdc  7074  enumctlemm  7075  enumct  7076  nnnninfeq  7088  nninfisol  7093  enomnilem  7098  fodju0  7107  enmkvlem  7121  enwomnilem  7129  exmidfodomrlemim  7153  exmidontriimlem2  7174  cc3  7205  dfplpq2  7291  nqpi  7315  nqnq0pi  7375  nq0nn  7379  elinp  7411  elnp1st2nd  7413  genprndl  7458  genprndu  7459  addnqprllem  7464  addnqprulem  7465  addnqprl  7466  addnqpru  7467  addlocpr  7473  nqprloc  7482  prmuloc  7503  mulnqprl  7505  mulnqpru  7506  mullocpr  7508  distrlem1prl  7519  distrlem1pru  7520  ltsopr  7533  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemloc  7544  ltexprlemrl  7547  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  recexprlemloc  7568  recexprlem1ssl  7570  recexprlem1ssu  7571  aptiprleml  7576  aptiprlemu  7577  archpr  7580  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlemladdru  7593  archrecpr  7601  caucvgprlemnkj  7603  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemladdfu  7614  caucvgprprlemnkltj  7626  caucvgprprlemnkeqj  7627  caucvgprprlemnjltk  7628  caucvgprprlemml  7631  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemdisj  7639  caucvgprprlemexbt  7643  caucvgprprlemexb  7644  caucvgprprlemaddq  7645  suplocexprlemru  7656  suplocexprlemloc  7658  suplocexprlemex  7659  suplocexprlemub  7660  suplocexprlemlub  7661  mulgt0sr  7715  caucvgsrlemcau  7730  caucvgsrlemoffcau  7735  caucvgsrlemoffres  7737  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  axcaucvglemcau  7835  axcaucvglemres  7836  axpre-suploclemres  7838  axsuploc  7967  cnegexlem1  8069  cnegex  8072  apsym  8500  apcotr  8501  apadd1  8502  mulext1  8506  mulge0  8513  apti  8516  aprcl  8540  conjmulap  8621  lemulge11  8757  creui  8851  nndiv  8894  zaddcllemneg  9226  suprzclex  9285  eluzuzle  9470  infregelbex  9532  divfnzn  9555  qapne  9573  xrltso  9728  xnn0dcle  9734  xnn0letri  9735  xrre  9752  xrre3  9754  xaddf  9776  xaddval  9777  xpncan  9803  xleadd1a  9805  xltadd1  9808  xleaddadd  9819  ixxss12  9838  elioc2  9868  elico2  9869  elicc2  9870  fzm1  10031  fzneuz  10032  eluzgtdifelfzo  10128  elfzonelfzo  10161  exfzdc  10171  qtri3or  10174  exbtwnzlemstep  10179  exbtwnzlemex  10181  exbtwnz  10182  modqid  10280  modqcyc2  10291  modqmuladd  10297  modqmuladdnn0  10299  modaddmodlo  10319  addmodlteq  10329  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgsuc  10345  frecuzrdgsuctlem  10354  seq3clss  10398  iseqf1olemqcl  10417  iseqf1olemnab  10419  iseqf1olemab  10420  iseqf1olemmo  10423  iseqf1olemqf1o  10424  iseqf1olemjpcl  10426  iseqf1olemqpcl  10427  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3f1olemp  10433  seq3f1oleml  10434  seq3f1o  10435  seq3id3  10438  ser3ge0  10448  exp3val  10453  expap0  10481  qsqeqor  10561  modqexp  10577  nn0ltexp2  10619  facndiv  10648  faclbnd  10650  bcval5  10672  hashunlem  10713  hashun  10714  hashprg  10717  fiprsshashgt1  10726  hashfacen  10745  zfz1isolemiso  10748  zfz1isolem1  10749  seq3coll  10751  ovshftex  10757  2shfti  10769  seq3shft  10776  cjap  10844  caucvgrelemcau  10918  cvg1nlemcau  10922  cvg1nlemres  10923  recvguniq  10933  resqrexlemdecn  10950  resqrexlemcalc3  10954  resqrexlemcvg  10957  resqrexlemoverl  10959  leabs  11012  absexpzap  11018  ltabs  11025  abslt  11026  absle  11027  maxleim  11143  maxabslemval  11146  fimaxre2  11164  minmax  11167  2zinfmin  11180  xrmaxiflemcl  11182  xrmaxifle  11183  xrmaxiflemab  11184  xrmaxiflemlub  11185  xrmaxiflemcom  11186  xrmaxltsup  11195  xrmaxadd  11198  xrminmax  11202  xrbdtri  11213  2clim  11238  climshftlemg  11239  climsqz  11272  climsqz2  11273  climrecvg1n  11285  climcvg1nlem  11286  serf0  11289  sumrbdclem  11314  fsum3cvg  11315  summodclem3  11317  summodclem2a  11318  summodclem2  11319  zsumdc  11321  fsum3  11324  isumss  11328  fisumss  11329  fsum3cvg3  11333  fsumcl2lem  11335  fsumadd  11343  fsumsplit  11344  sumsnf  11346  fsum2d  11372  fisum0diag2  11384  fsummulc2  11385  modfsummod  11395  fsumabs  11402  fsumrelem  11408  fsumiun  11414  geoisumr  11455  cvgratnnlemseq  11463  cvgratz  11469  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodrbdclem  11508  fproddccvg  11509  prodmodclem3  11512  prodmodclem2a  11513  zproddc  11516  fprodseq  11520  fprodntrivap  11521  fprodssdc  11527  fprodmul  11528  prodsnf  11529  fprodsplitdc  11533  fprodsplit  11534  fprodunsn  11541  fprodcl2lem  11542  fprodap0  11558  fprod2d  11560  fprodrec  11566  fprodap0f  11573  efcj  11610  efaddlem  11611  tanaddaplem  11675  nndivides  11733  dvdsext  11789  divalglemeunn  11854  divalglemex  11855  divalglemeuneg  11856  zsupcllemstep  11874  infssuzex  11878  suprzubdc  11881  nninfdcex  11882  zsupssdc  11883  dvdsbnd  11885  bezoutlemnewy  11925  bezoutlemstep  11926  bezoutlemmain  11927  bezoutlemzz  11931  bezoutlemaz  11932  bezoutlembz  11933  bezoutlemeu  11936  bezoutlemle  11937  bezoutlemsup  11938  dfgcd3  11939  dfgcd2  11943  bezoutr1  11962  nnmindc  11963  dvdslcm  11997  lcmgcdlem  12005  qredeq  12024  qredeu  12025  divgcdcoprm0  12029  divgcdcoprmex  12030  cncongr1  12031  isprm2lem  12044  prmind2  12048  exprmfct  12066  prmdvdsfz  12067  isprm5lem  12069  prmexpb  12079  rpexp1i  12082  sqrt2irr  12090  sqne2sq  12105  nonsq  12135  phiprmpw  12150  eulerthlemrprm  12157  eulerthlema  12158  hashgcdeq  12167  phisum  12168  modprmn0modprm0  12184  pclemub  12215  pclemdc  12216  pcmul  12229  pcqmul  12231  pcdvdstr  12254  pcprmpw2  12260  difsqpwdvds  12265  pcmpt  12269  oddprmdvds  12280  prmpwdvds  12281  pockthg  12283  infpnlem1  12285  1arith  12293  4sqlem2  12315  ennnfonelemg  12332  ennnfoneleminc  12340  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemfun  12346  ennnfonelemf1  12347  ennnfonelemrn  12348  ennnfonelemdm  12349  ennnfonelemnn0  12351  ennnfonelemim  12353  exmidunben  12355  ctinfomlemom  12356  ctinf  12359  ctiunctlemudc  12366  nninfdclemlt  12380  nninfdclemf1  12381  isstruct2r  12401  tgdom  12672  neipsm  12754  tgrest  12769  cnfval  12794  cnpfval  12795  cnpval  12798  iscnp4  12818  cnpnei  12819  cnptopco  12822  cncnpi  12828  cncnp  12830  cnptopresti  12838  cnptoprest2  12840  cndis  12841  lmtopcnp  12850  txbasval  12867  neitx  12868  txcnp  12871  txcnmpt  12873  txcn  12875  imasnopn  12899  psmetres2  12933  isxmet2d  12948  xblss2ps  13004  xblss2  13005  blbas  13033  neibl  13091  metss2lem  13097  metrest  13106  xmettx  13110  metcnp3  13111  metcnp  13112  metcnp2  13113  metcnpi  13115  metcnpi2  13116  mulc1cncf  13176  cncfco  13178  mulcncflem  13190  mulcncf  13191  dedekindeulemuub  13195  dedekindeulemloc  13197  dedekindeulemlu  13199  dedekindeu  13201  suplociccreex  13202  suplociccex  13203  dedekindicclemuub  13204  dedekindicclemloc  13206  dedekindicclemlu  13208  dedekindicclemicc  13210  dedekindicc  13211  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemloc  13219  ivthinc  13221  limcimolemlt  13233  limccnp2lem  13245  limccnp2cntop  13246  limccoap  13247  dvcj  13273  dveflem  13287  efltlemlt  13295  sin0pilem1  13302  sin0pilem2  13303  pilem3  13304  coseq0negpitopi  13357  abssinper  13367  cos02pilt1  13372  relogeftb  13386  logbgcd1irraplemexp  13486  logbgcd1irrap  13488  lgsval  13505  lgsfvalg  13506  lgsfcl2  13507  lgsval2lem  13511  lgsmod  13527  lgsdilem  13528  lgsdir2lem4  13532  lgsdir2  13534  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  lgsdirnn0  13548  lgsdinn0  13549  2sqlem5  13555  2sqlem6  13556  2sqlem7  13557  2sqlem9  13560  2sqlem10  13561  bj-findis  13821  pwle2  13838  pwf1oexmid  13839  pw1nct  13843  nnsf  13845  peano4nninf  13846  nninfall  13849  nninfsellemeq  13854  nninfsellemeqinf  13856  qdencn  13866  refeq  13867  trilpolemeq1  13879  trilpolemlt1  13880  trirec0  13883  nconstwlpolemgt0  13902  nconstwlpolem  13903  neapmkvlem  13905