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  4340  frirrg  4440  ralxfrd  4552  nnsucpred  4708  foun  5590  f1oprg  5616  dffo4  5782  funopsn  5816  foeqcnvco  5913  fliftfun  5919  isotr  5939  riotass2  5982  ovmpodxf  6129  mpoxopoveq  6384  tfrlem1  6452  tfrlemibacc  6470  tfrlemibfn  6472  tfrlemi14d  6477  tfrexlem  6478  tfr1onlembacc  6486  tfr1onlembfn  6488  tfr1onlemres  6493  tfrcllembacc  6499  tfrcllembfn  6501  tfrcllemres  6506  frecabcl  6543  nnmordi  6660  eroprf  6773  f1imaen2g  6943  pw2f1odclem  6991  xpen  7002  mapen  7003  mapdom1g  7004  mapxpen  7005  xpmapenlem  7006  phplem4dom  7019  nndomo  7021  phpm  7023  fidifsnen  7028  dif1enen  7038  fisbth  7041  fimax2gtrilemstep  7058  fimax2gtri  7059  en2eqpr  7065  unsnfidcex  7078  unsnfidcel  7079  ssfirab  7094  fidcenumlemrks  7116  sbthlemi8  7127  fiuni  7141  ordiso2  7198  updjud  7245  difinfsnlem  7262  ctssdclemn0  7273  ctssdccl  7274  ctssdc  7276  enumctlemm  7277  enumct  7278  nnnninfeq  7291  nninfisol  7296  enomnilem  7301  fodju0  7310  enmkvlem  7324  enwomnilem  7332  nninfwlpoimlemg  7338  pr1or2  7363  pr2cv1  7364  exmidfodomrlemim  7375  exmidontriimlem2  7400  exmidapne  7442  cc3  7450  dfplpq2  7537  nqpi  7561  nqnq0pi  7621  nq0nn  7625  elinp  7657  elnp1st2nd  7659  genprndl  7704  genprndu  7705  addnqprllem  7710  addnqprulem  7711  addnqprl  7712  addnqpru  7713  addlocpr  7719  nqprloc  7728  prmuloc  7749  mulnqprl  7751  mulnqpru  7752  mullocpr  7754  distrlem1prl  7765  distrlem1pru  7766  ltsopr  7779  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemloc  7790  ltexprlemrl  7793  ltexprlemru  7795  addcanprleml  7797  addcanprlemu  7798  recexprlemloc  7814  recexprlem1ssl  7816  recexprlem1ssu  7817  aptiprleml  7822  aptiprlemu  7823  archpr  7826  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlemladdru  7839  archrecpr  7847  caucvgprlemnkj  7849  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemladdfu  7860  caucvgprprlemnkltj  7872  caucvgprprlemnkeqj  7873  caucvgprprlemnjltk  7874  caucvgprprlemml  7877  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemdisj  7885  caucvgprprlemexbt  7889  caucvgprprlemexb  7890  caucvgprprlemaddq  7891  suplocexprlemru  7902  suplocexprlemloc  7904  suplocexprlemex  7905  suplocexprlemub  7906  suplocexprlemlub  7907  mulgt0sr  7961  caucvgsrlemcau  7976  caucvgsrlemoffcau  7981  caucvgsrlemoffres  7983  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  axcaucvglemcau  8081  axcaucvglemres  8082  axpre-suploclemres  8084  axsuploc  8215  cnegexlem1  8317  cnegex  8320  apsym  8749  apcotr  8750  apadd1  8751  mulext1  8755  mulge0  8762  apti  8765  aprcl  8789  conjmulap  8872  lemulge11  9009  creui  9103  nndiv  9147  zaddcllemneg  9481  suprzclex  9541  eluzuzle  9726  infregelbex  9789  divfnzn  9812  qapne  9830  xrltso  9988  xnn0dcle  9994  xnn0letri  9995  xrre  10012  xrre3  10014  xaddf  10036  xaddval  10037  xpncan  10063  xleadd1a  10065  xltadd1  10068  xleaddadd  10079  ixxss12  10098  elioc2  10128  elico2  10129  elicc2  10130  fzm1  10292  fzneuz  10293  eluzgtdifelfzo  10398  elfzonelfzo  10431  exfzdc  10441  zsupcllemstep  10444  infssuzex  10448  suprzubdc  10451  nninfdcex  10452  zsupssdc  10453  qtri3or  10455  exbtwnzlemstep  10462  exbtwnzlemex  10464  exbtwnz  10465  modqid  10566  modqcyc2  10577  modqmuladd  10583  modqmuladdnn0  10585  modaddmodlo  10605  addmodlteq  10615  frecuzrdgrrn  10625  frec2uzrdg  10626  frecuzrdgsuc  10631  frecuzrdgsuctlem  10640  nninfinf  10660  seq3clss  10688  iseqf1olemqcl  10716  iseqf1olemnab  10718  iseqf1olemab  10719  iseqf1olemmo  10722  iseqf1olemqf1o  10723  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  seq3f1olemqsumk  10729  seq3f1olemqsum  10730  seq3f1olemp  10732  seq3f1oleml  10733  seq3f1o  10734  seqf1oglem1  10736  seqf1oglem2  10737  seqf1og  10738  seq3id3  10741  seqfeq4g  10748  ser3ge0  10753  exp3val  10758  expap0  10786  qsqeqor  10867  modqexp  10883  nn0ltexp2  10926  facndiv  10956  faclbnd  10958  bcval5  10980  hashunlem  11021  hashun  11022  hashprg  11025  fiprsshashgt1  11034  hashfacen  11053  zfz1isolemiso  11056  zfz1isolem1  11057  seq3coll  11059  ccatcl  11123  ccatlen  11125  ccatvalfn  11131  ccatsymb  11132  ccatrn  11139  swrdclg  11177  swrdspsleq  11194  pfxeq  11223  swrdswrd  11232  wrdind  11249  wrd2ind  11250  swrdccatin1  11252  swrdccatin2  11256  pfxccatin12  11260  pfxccat3  11261  swrdccat3b  11267  reuccatpfxs1  11274  ovshftex  11325  2shfti  11337  seq3shft  11344  cjap  11412  caucvgrelemcau  11486  cvg1nlemcau  11490  cvg1nlemres  11491  recvguniq  11501  resqrexlemdecn  11518  resqrexlemcalc3  11522  resqrexlemcvg  11525  resqrexlemoverl  11527  leabs  11580  absexpzap  11586  ltabs  11593  abslt  11594  absle  11595  maxleim  11711  maxabslemval  11714  fimaxre2  11733  minmax  11736  2zinfmin  11749  xrmaxiflemcl  11751  xrmaxifle  11752  xrmaxiflemab  11753  xrmaxiflemlub  11754  xrmaxiflemcom  11755  xrmaxltsup  11764  xrmaxadd  11767  xrminmax  11771  xrbdtri  11782  2clim  11807  climshftlemg  11808  climsqz  11841  climsqz2  11842  climrecvg1n  11854  climcvg1nlem  11855  serf0  11858  sumrbdclem  11883  fsum3cvg  11884  summodclem3  11886  summodclem2a  11887  summodclem2  11888  zsumdc  11890  fsum3  11893  isumss  11897  fisumss  11898  fsum3cvg3  11902  fsumcl2lem  11904  fsumadd  11912  fsumsplit  11913  sumsnf  11915  fsum2d  11941  fisum0diag2  11953  fsummulc2  11954  modfsummod  11964  fsumabs  11971  fsumrelem  11977  fsumiun  11983  geoisumr  12024  cvgratnnlemseq  12032  cvgratz  12038  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodrbdclem  12077  fproddccvg  12078  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  fprodntrivap  12090  fprodssdc  12096  fprodmul  12097  prodsnf  12098  fprodsplitdc  12102  fprodsplit  12103  fprodunsn  12110  fprodcl2lem  12111  fprodap0  12127  fprod2d  12129  fprodrec  12135  fprodap0f  12142  efcj  12179  efaddlem  12180  tanaddaplem  12244  sinltxirr  12267  nndivides  12303  dvdsext  12361  divalglemeunn  12427  divalglemex  12428  divalglemeuneg  12429  bitsfzolem  12460  bitsmod  12462  bitsinv1  12468  dvdsbnd  12472  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemmain  12514  bezoutlemzz  12518  bezoutlemaz  12519  bezoutlembz  12520  bezoutlemeu  12523  bezoutlemle  12524  bezoutlemsup  12525  dfgcd3  12526  dfgcd2  12530  bezoutr1  12549  nnmindc  12550  nninfctlemfo  12556  dvdslcm  12586  lcmgcdlem  12594  qredeq  12613  qredeu  12614  divgcdcoprm0  12618  divgcdcoprmex  12619  cncongr1  12620  isprm2lem  12633  prmind2  12637  exprmfct  12655  prmdvdsfz  12656  isprm5lem  12658  prmexpb  12668  rpexp1i  12671  sqrt2irr  12679  sqne2sq  12694  nonsq  12724  phiprmpw  12739  eulerthlemrprm  12746  eulerthlema  12747  hashgcdeq  12757  phisum  12758  modprmn0modprm0  12774  pclemub  12805  pclemdc  12806  pcmul  12819  pcqmul  12821  pcxqcl  12830  pcdvdstr  12845  pcprmpw2  12851  difsqpwdvds  12856  pcmpt  12861  oddprmdvds  12872  prmpwdvds  12873  pockthg  12875  infpnlem1  12877  1arith  12885  4sqlem2  12907  4sqlemafi  12913  4sqlemffi  12914  4sqleminfi  12915  4sqlem11  12919  4sqlem13m  12921  4sqlem14  12922  4sqlem17  12925  4sqlem18  12926  ennnfonelemg  12969  ennnfoneleminc  12977  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemex  12980  ennnfonelemhom  12981  ennnfonelemfun  12983  ennnfonelemf1  12984  ennnfonelemrn  12985  ennnfonelemdm  12986  ennnfonelemnn0  12988  ennnfonelemim  12990  exmidunben  12992  ctinfomlemom  12993  ctinf  12996  ctiunctlemudc  13003  nninfdclemlt  13017  nninfdclemf1  13018  isstruct2r  13038  prdsval  13301  imasival  13334  gsumpropd2  13421  sgrppropd  13441  prdssgrpd  13443  mndpropd  13468  issubmnd  13470  prdsidlem  13475  prdsmndd  13476  pws0g  13479  mndissubm  13503  resmhm2b  13517  mhmeql  13520  gsumfzz  13523  gsumwsubmcl  13524  gsumwmhm  13526  gsumfzcl  13527  grpinvnz  13599  pwssub  13641  mhmmnd  13648  mulgfng  13656  mulgz  13682  mulgnndir  13683  mulgnn0dir  13684  mulgneg2  13688  mulgass  13691  mhmmulg  13695  issubgrpd2  13722  issubg4m  13725  grpissubg  13726  isnsg3  13739  ghmpreima  13798  ghmnsgpreima  13801  ghmf1  13805  conjnmz  13811  conjnmzb  13812  eqgabl  13862  gsumfzreidx  13869  gsumfzsubmcl  13870  gsumfzmptfidmadd  13871  gsumfzmhm  13875  rngpropd  13913  issrg  13923  ringpropd  13996  ringinvnz1ne0  14007  dvdsrvald  14051  dvdsrd  14052  dvdsrtr  14059  unitgrp  14074  rhmopp  14134  lmodfopne  14284  lmodprop2d  14306  lssvacl  14323  lsslss  14339  lss1d  14341  lsspropdg  14389  rnglidlmcl  14438  lidlacl  14442  isridl  14462  znidomb  14616  znunit  14617  znrrg  14618  psrval  14624  mplsubgfilemcl  14657  mplsubgfileminv  14658  mplsubgfi  14659  tgdom  14740  neipsm  14822  tgrest  14837  cnfval  14862  cnpfval  14863  cnpval  14866  iscnp4  14886  cnpnei  14887  cnptopco  14890  cncnpi  14896  cncnp  14898  cnptopresti  14906  cnptoprest2  14908  cndis  14909  lmtopcnp  14918  txbasval  14935  neitx  14936  txcnp  14939  txcnmpt  14941  txcn  14943  imasnopn  14967  psmetres2  15001  isxmet2d  15016  xblss2ps  15072  xblss2  15073  blbas  15101  neibl  15159  metss2lem  15165  metrest  15174  xmettx  15178  metcnp3  15179  metcnp  15180  metcnp2  15181  metcnpi  15183  metcnpi2  15184  mulc1cncf  15257  cncfco  15259  mulcncflem  15275  mulcncf  15276  dedekindeulemuub  15285  dedekindeulemloc  15287  dedekindeulemlu  15289  dedekindeu  15291  suplociccreex  15292  suplociccex  15293  dedekindicclemuub  15294  dedekindicclemloc  15296  dedekindicclemlu  15298  dedekindicclemicc  15300  dedekindicc  15301  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemloc  15309  ivthinc  15311  limcimolemlt  15332  limccnp2lem  15344  limccnp2cntop  15345  limccoap  15346  dvcj  15377  dvmptfsum  15393  dveflem  15394  plyf  15405  plyaddlem1  15415  plymullem1  15416  plycolemc  15426  plyco  15427  plycj  15429  dvply1  15433  dvply2g  15434  efltlemlt  15442  sin0pilem1  15449  sin0pilem2  15450  pilem3  15451  coseq0negpitopi  15504  abssinper  15514  cos02pilt1  15519  relogeftb  15533  logbgcd1irraplemexp  15636  logbgcd1irrap  15638  dvdsppwf1o  15657  mpodvdsmulf1o  15658  mersenne  15665  perfectlem2  15668  perfect  15669  lgsval  15677  lgsfvalg  15678  lgsfcl2  15679  lgsval2lem  15683  lgsmod  15699  lgsdilem  15700  lgsdir2lem4  15704  lgsdir2  15706  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  lgsdirnn0  15720  lgsdinn0  15721  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem2  15755  2lgslem1a1  15759  2lgslem1a  15761  2sqlem5  15792  2sqlem6  15793  2sqlem7  15794  2sqlem9  15797  2sqlem10  15798  umgrnloopv  15908  uhgr2edg  15998  bj-findis  16300  2omap  16318  pwle2  16323  pwf1oexmid  16324  pw1nct  16328  nnsf  16330  peano4nninf  16331  nninfall  16334  nninfsellemeq  16339  nninfsellemeqinf  16341  nnnninfex  16347  nninfnfiinf  16348  qdencn  16354  refeq  16355  trilpolemeq1  16367  trilpolemlt1  16368  trirec0  16371  nconstwlpolemgt0  16391  nconstwlpolem  16392  neapmkvlem  16394