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  1266  vtoclgft  2855  reupick  3493  euotd  4353  frirrg  4453  ralxfrd  4565  nnsucpred  4721  foun  5611  f1oprg  5638  dffo4  5803  funopsn  5838  foeqcnvco  5941  fliftfun  5947  isotr  5967  riotass2  6010  ovmpodxf  6157  suppfnss  6435  suppcofn  6444  mpoxopoveq  6449  tfrlem1  6517  tfrlemibacc  6535  tfrlemibfn  6537  tfrlemi14d  6542  tfrexlem  6543  tfr1onlembacc  6551  tfr1onlembfn  6553  tfr1onlemres  6558  tfrcllembacc  6564  tfrcllembfn  6566  tfrcllemres  6571  frecabcl  6608  nnmordi  6727  eroprf  6840  f1imaen2g  7010  pw2f1odclem  7063  xpen  7074  mapen  7075  mapdom1g  7076  mapxpen  7077  xpmapenlem  7078  phplem4dom  7091  nndomo  7093  phpm  7095  fidifsnen  7100  dif1enen  7112  fisbth  7115  fimax2gtrilemstep  7133  fimax2gtri  7134  eqsndc  7138  en2eqpr  7142  unsnfidcex  7155  unsnfidcel  7156  ssfirab  7172  fidcenumlemrks  7195  sbthlemi8  7206  fiuni  7220  ordiso2  7277  updjud  7324  difinfsnlem  7341  ctssdclemn0  7352  ctssdccl  7353  ctssdc  7355  enumctlemm  7356  enumct  7357  nnnninfeq  7370  nninfisol  7375  enomnilem  7380  fodju0  7389  enmkvlem  7403  enwomnilem  7411  nninfwlpoimlemg  7417  pr1or2  7442  pr2cv1  7443  exmidfodomrlemim  7455  exmidontriimlem2  7480  exmidapne  7522  cc3  7530  dfplpq2  7617  nqpi  7641  nqnq0pi  7701  nq0nn  7705  elinp  7737  elnp1st2nd  7739  genprndl  7784  genprndu  7785  addnqprllem  7790  addnqprulem  7791  addnqprl  7792  addnqpru  7793  addlocpr  7799  nqprloc  7808  prmuloc  7829  mulnqprl  7831  mulnqpru  7832  mullocpr  7834  distrlem1prl  7845  distrlem1pru  7846  ltsopr  7859  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemloc  7870  ltexprlemrl  7873  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  recexprlemloc  7894  recexprlem1ssl  7896  recexprlem1ssu  7897  aptiprleml  7902  aptiprlemu  7903  archpr  7906  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  archrecpr  7927  caucvgprlemnkj  7929  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemladdfu  7940  caucvgprprlemnkltj  7952  caucvgprprlemnkeqj  7953  caucvgprprlemnjltk  7954  caucvgprprlemml  7957  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemdisj  7965  caucvgprprlemexbt  7969  caucvgprprlemexb  7970  caucvgprprlemaddq  7971  suplocexprlemru  7982  suplocexprlemloc  7984  suplocexprlemex  7985  suplocexprlemub  7986  suplocexprlemlub  7987  mulgt0sr  8041  caucvgsrlemcau  8056  caucvgsrlemoffcau  8061  caucvgsrlemoffres  8063  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  axcaucvglemcau  8161  axcaucvglemres  8162  axpre-suploclemres  8164  axsuploc  8294  cnegexlem1  8396  cnegex  8399  apsym  8828  apcotr  8829  apadd1  8830  mulext1  8834  mulge0  8841  apti  8844  aprcl  8868  conjmulap  8951  lemulge11  9088  creui  9182  nndiv  9226  zaddcllemneg  9562  suprzclex  9622  eluzuzle  9808  infregelbex  9876  divfnzn  9899  qapne  9917  xrltso  10075  xnn0dcle  10081  xnn0letri  10082  xrre  10099  xrre3  10101  xaddf  10123  xaddval  10124  xpncan  10150  xleadd1a  10152  xltadd1  10155  xleaddadd  10166  ixxss12  10185  elioc2  10215  elico2  10216  elicc2  10217  fzm1  10380  fzneuz  10381  eluzgtdifelfzo  10488  elfzonelfzo  10521  exfzdc  10532  zsupcllemstep  10535  infssuzex  10539  suprzubdc  10542  nninfdcex  10543  zsupssdc  10544  qtri3or  10546  exbtwnzlemstep  10553  exbtwnzlemex  10555  exbtwnz  10556  modqid  10657  modqcyc2  10668  modqmuladd  10674  modqmuladdnn0  10676  modaddmodlo  10696  addmodlteq  10706  frecuzrdgrrn  10716  frec2uzrdg  10717  frecuzrdgsuc  10722  frecuzrdgsuctlem  10731  nninfinf  10751  seq3clss  10779  iseqf1olemqcl  10807  iseqf1olemnab  10809  iseqf1olemab  10810  iseqf1olemmo  10813  iseqf1olemqf1o  10814  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  seq3f1olemqsumk  10820  seq3f1olemqsum  10821  seq3f1olemp  10823  seq3f1oleml  10824  seq3f1o  10825  seqf1oglem1  10827  seqf1oglem2  10828  seqf1og  10829  seq3id3  10832  seqfeq4g  10839  ser3ge0  10844  exp3val  10849  expap0  10877  qsqeqor  10958  modqexp  10974  nn0ltexp2  11017  facndiv  11047  faclbnd  11049  bcval5  11071  hashunlem  11113  hashun  11114  hashprg  11118  fiprsshashgt1  11127  hashfacen  11146  zfz1isolemiso  11149  zfz1isolem1  11150  seq3coll  11152  hashtpglem  11156  ccatcl  11219  ccatlen  11221  ccatvalfn  11227  ccatsymb  11228  ccatrn  11235  ccat2s1fstg  11274  swrdclg  11280  swrdspsleq  11297  pfxeq  11326  swrdswrd  11335  wrdind  11352  wrd2ind  11353  swrdccatin1  11355  swrdccatin2  11359  pfxccatin12  11363  pfxccat3  11364  swrdccat3b  11370  reuccatpfxs1  11377  ovshftex  11442  2shfti  11454  seq3shft  11461  cjap  11529  caucvgrelemcau  11603  cvg1nlemcau  11607  cvg1nlemres  11608  recvguniq  11618  resqrexlemdecn  11635  resqrexlemcalc3  11639  resqrexlemcvg  11642  resqrexlemoverl  11644  leabs  11697  absexpzap  11703  ltabs  11710  abslt  11711  absle  11712  maxleim  11828  maxabslemval  11831  fimaxre2  11850  minmax  11853  2zinfmin  11866  xrmaxiflemcl  11868  xrmaxifle  11869  xrmaxiflemab  11870  xrmaxiflemlub  11871  xrmaxiflemcom  11872  xrmaxltsup  11881  xrmaxadd  11884  xrminmax  11888  xrbdtri  11899  2clim  11924  climshftlemg  11925  climsqz  11958  climsqz2  11959  climrecvg1n  11971  climcvg1nlem  11972  serf0  11975  sumrbdclem  12001  fsum3cvg  12002  summodclem3  12004  summodclem2a  12005  summodclem2  12006  zsumdc  12008  fsum3  12011  isumss  12015  fisumss  12016  fsum3cvg3  12020  fsumcl2lem  12022  fsumadd  12030  fsumsplit  12031  sumsnf  12033  fsum2d  12059  fisum0diag2  12071  fsummulc2  12072  modfsummod  12082  fsumabs  12089  fsumrelem  12095  fsumiun  12101  geoisumr  12142  cvgratnnlemseq  12150  cvgratz  12156  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  prodrbdclem  12195  fproddccvg  12196  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodntrivap  12208  fprodssdc  12214  fprodmul  12215  prodsnf  12216  fprodsplitdc  12220  fprodsplit  12221  fprodunsn  12228  fprodcl2lem  12229  fprodap0  12245  fprod2d  12247  fprodrec  12253  fprodap0f  12260  efcj  12297  efaddlem  12298  tanaddaplem  12362  sinltxirr  12385  nndivides  12421  dvdsext  12479  divalglemeunn  12545  divalglemex  12546  divalglemeuneg  12547  bitsfzolem  12578  bitsmod  12580  bitsinv1  12586  dvdsbnd  12590  bezoutlemnewy  12630  bezoutlemstep  12631  bezoutlemmain  12632  bezoutlemzz  12636  bezoutlemaz  12637  bezoutlembz  12638  bezoutlemeu  12641  bezoutlemle  12642  bezoutlemsup  12643  dfgcd3  12644  dfgcd2  12648  bezoutr1  12667  nnmindc  12668  nninfctlemfo  12674  dvdslcm  12704  lcmgcdlem  12712  qredeq  12731  qredeu  12732  divgcdcoprm0  12736  divgcdcoprmex  12737  cncongr1  12738  isprm2lem  12751  prmind2  12755  exprmfct  12773  prmdvdsfz  12774  isprm5lem  12776  prmexpb  12786  rpexp1i  12789  sqrt2irr  12797  sqne2sq  12812  nonsq  12842  phiprmpw  12857  eulerthlemrprm  12864  eulerthlema  12865  hashgcdeq  12875  phisum  12876  modprmn0modprm0  12892  pclemub  12923  pclemdc  12924  pcmul  12937  pcqmul  12939  pcxqcl  12948  pcdvdstr  12963  pcprmpw2  12969  difsqpwdvds  12974  pcmpt  12979  oddprmdvds  12990  prmpwdvds  12991  pockthg  12993  infpnlem1  12995  1arith  13003  4sqlem2  13025  4sqlemafi  13031  4sqlemffi  13032  4sqleminfi  13033  4sqlem11  13037  4sqlem13m  13039  4sqlem14  13040  4sqlem17  13043  4sqlem18  13044  ennnfonelemg  13087  ennnfoneleminc  13095  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemfun  13101  ennnfonelemf1  13102  ennnfonelemrn  13103  ennnfonelemdm  13104  ennnfonelemnn0  13106  ennnfonelemim  13108  exmidunben  13110  ctinfomlemom  13111  ctinf  13114  ctiunctlemudc  13121  nninfdclemlt  13135  nninfdclemf1  13136  isstruct2r  13156  prdsval  13419  imasival  13452  gsumpropd2  13539  sgrppropd  13559  prdssgrpd  13561  mndpropd  13586  issubmnd  13588  prdsidlem  13593  prdsmndd  13594  pws0g  13597  mndissubm  13621  resmhm2b  13635  mhmeql  13638  gsumfzz  13641  gsumwsubmcl  13642  gsumwmhm  13644  gsumfzcl  13645  grpinvnz  13717  pwssub  13759  mhmmnd  13766  mulgfng  13774  mulgz  13800  mulgnndir  13801  mulgnn0dir  13802  mulgneg2  13806  mulgass  13809  mhmmulg  13813  issubgrpd2  13840  issubg4m  13843  grpissubg  13844  isnsg3  13857  ghmpreima  13916  ghmnsgpreima  13919  ghmf1  13923  conjnmz  13929  conjnmzb  13930  eqgabl  13980  gsumfzreidx  13987  gsumfzsubmcl  13988  gsumfzmptfidmadd  13989  gsumfzmhm  13993  rngpropd  14032  issrg  14042  ringpropd  14115  ringinvnz1ne0  14126  dvdsrvald  14171  dvdsrd  14172  dvdsrtr  14179  unitgrp  14194  rhmopp  14254  lmodfopne  14405  lmodprop2d  14427  lssvacl  14444  lsslss  14460  lss1d  14462  lsspropdg  14510  rnglidlmcl  14559  lidlacl  14563  isridl  14583  znidomb  14737  znunit  14738  znrrg  14739  psrval  14745  mplsubgfilemcl  14783  mplsubgfileminv  14784  mplsubgfi  14785  tgdom  14866  neipsm  14948  tgrest  14963  cnfval  14988  cnpfval  14989  cnpval  14992  iscnp4  15012  cnpnei  15013  cnptopco  15016  cncnpi  15022  cncnp  15024  cnptopresti  15032  cnptoprest2  15034  cndis  15035  lmtopcnp  15044  txbasval  15061  neitx  15062  txcnp  15065  txcnmpt  15067  txcn  15069  imasnopn  15093  psmetres2  15127  isxmet2d  15142  xblss2ps  15198  xblss2  15199  blbas  15227  neibl  15285  metss2lem  15291  metrest  15300  xmettx  15304  metcnp3  15305  metcnp  15306  metcnp2  15307  metcnpi  15309  metcnpi2  15310  mulc1cncf  15383  cncfco  15385  mulcncflem  15401  mulcncf  15402  dedekindeulemuub  15411  dedekindeulemloc  15413  dedekindeulemlu  15415  dedekindeu  15417  suplociccreex  15418  suplociccex  15419  dedekindicclemuub  15420  dedekindicclemloc  15422  dedekindicclemlu  15424  dedekindicclemicc  15426  dedekindicc  15427  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemloc  15435  ivthinc  15437  limcimolemlt  15458  limccnp2lem  15470  limccnp2cntop  15471  limccoap  15472  dvcj  15503  dvmptfsum  15519  dveflem  15520  plyf  15531  plyaddlem1  15541  plymullem1  15542  plycolemc  15552  plyco  15553  plycj  15555  dvply1  15559  dvply2g  15560  efltlemlt  15568  sin0pilem1  15575  sin0pilem2  15576  pilem3  15577  coseq0negpitopi  15630  abssinper  15640  cos02pilt1  15645  relogeftb  15659  logbgcd1irraplemexp  15762  logbgcd1irrap  15764  dvdsppwf1o  15786  mpodvdsmulf1o  15787  mersenne  15794  perfectlem2  15797  perfect  15798  lgsval  15806  lgsfvalg  15807  lgsfcl2  15808  lgsval2lem  15812  lgsmod  15828  lgsdilem  15829  lgsdir2lem4  15833  lgsdir2  15835  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem1a  15860  gausslemma2dlem1f1o  15862  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem2  15884  2lgslem1a1  15888  2lgslem1a  15890  2sqlem5  15921  2sqlem6  15922  2sqlem7  15923  2sqlem9  15926  2sqlem10  15927  umgrnloopv  16038  uhgr2edg  16130  upgredginwlk  16280  clwwlkccatlem  16324  eupth2lem3lem3fi  16394  eupth2lem3lem4fi  16397  eupth2lemsfi  16402  depindlem3  16432  bj-findis  16678  2omap  16698  pwle2  16703  pwf1oexmid  16704  pw1nct  16708  nnsf  16714  peano4nninf  16715  nninfall  16718  nninfsellemeq  16723  nninfsellemeqinf  16725  nnnninfex  16731  nninfnfiinf  16732  qdencn  16738  refeq  16739  trilpolemeq1  16755  trilpolemlt1  16756  trirec0  16759  nconstwlpolemgt0  16780  nconstwlpolem  16781  neapmkvlem  16783  gfsumval  16792  gfsumcl  16799