Theorem ad2antrr 492

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 481	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad3antrrr  496  ad5ant13  523  ad5ant23  526  simpll  531  simplll  539  simpllr  540  ad5ant123  1270  vtoclgft  2873  reupick  3517  ifeqeqxdc  3687  euotd  4397  frirrg  4497  ralxfrd  4610  nnsucpred  4766  foun  5661  f1oprg  5688  dffo4  5859  funopsn  5894  foeqcnvco  5999  fliftfun  6005  isotr  6025  riotass2  6070  ovmpodxf  6217  suppfnss  6501  suppcofn  6510  mpoxopoveq  6515  tfrlem1  6583  tfrlemibacc  6601  tfrlemibfn  6603  tfrlemi14d  6608  tfrexlem  6609  tfr1onlembacc  6617  tfr1onlembfn  6619  tfr1onlemres  6624  tfrcllembacc  6630  tfrcllembfn  6632  tfrcllemres  6637  frecabcl  6674  nnmordi  6793  eroprf  6906  mapsnd  6974  f1imaen2g  7084  pw2f1odclem  7138  xpen  7149  mapen  7150  mapdom1g  7151  mapxpen  7152  xpmapenlem  7153  phplem4dom  7167  nndomo  7169  phpm  7171  fidifsnen  7176  dif1enen  7188  fisbth  7191  fimax2gtrilemstep  7209  fimax2gtri  7210  eqsndc  7214  en2eqpr  7218  unsnfidcex  7231  unsnfidcel  7232  ssfirab  7248  fidcenumlemrks  7275  sbthlemi8  7286  fiuni  7317  2omap  7324  ordiso2  7381  updjud  7428  difinfsnlem  7445  ctssdclemn0  7456  ctssdccl  7457  ctssdc  7459  enumctlemm  7460  enumct  7461  nnnninfeq  7474  nninfisol  7479  enomnilem  7484  fodju0  7493  enmkvlem  7507  enwomnilem  7515  nninfwlpoimlemg  7521  pr1or2  7546  pr2cv1  7547  exmidfodomrlemim  7559  exmidontriimlem2  7584  exmidapne  7632  cc3  7640  dfplpq2  7727  nqpi  7751  nqnq0pi  7811  nq0nn  7815  elinp  7847  elnp1st2nd  7849  genprndl  7894  genprndu  7895  addnqprllem  7900  addnqprulem  7901  addnqprl  7902  addnqpru  7903  addlocpr  7909  nqprloc  7918  prmuloc  7939  mulnqprl  7941  mulnqpru  7942  mullocpr  7944  distrlem1prl  7955  distrlem1pru  7956  ltsopr  7969  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  aptiprleml  8012  aptiprlemu  8013  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  archrecpr  8037  caucvgprlemnkj  8039  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemnjltk  8064  caucvgprprlemml  8067  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemdisj  8075  caucvgprprlemexbt  8079  caucvgprprlemexb  8080  caucvgprprlemaddq  8081  suplocexprlemru  8092  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  suplocexprlemlub  8097  mulgt0sr  8151  caucvgsrlemcau  8166  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  axsuploc  8404  cnegexlem1  8508  cnegex  8511  apsym  8942  apcotr  8943  apadd1  8944  mulext1  8948  mulge0  8955  apti  8958  aprcl  8982  conjmulap  9067  lemulge11  9204  creui  9298  nndiv  9354  zaddcllemneg  9694  suprzclex  9755  eluzuzle  9946  infregelbex  10014  divfnzn  10037  qapne  10055  xrltso  10215  xnn0dcle  10221  xnn0letri  10222  xrre  10239  xrre3  10241  xaddf  10263  xaddval  10264  xpncan  10290  xleadd1a  10292  xltadd1  10295  xleaddadd  10306  ixxss12  10325  elioc2  10355  elico2  10356  elicc2  10357  fzm1  10524  fzneuz  10525  eluzgtdifelfzo  10632  elfzonelfzo  10665  exfzdc  10676  zsupcllemstep  10679  infssuzex  10683  suprzubdc  10688  nninfdcex  10689  zsupssdc  10690  qtri3or  10692  exbtwnzlemstep  10699  exbtwnzlemex  10701  exbtwnz  10702  flaplt  10739  modqid  10807  modqcyc2  10818  modqmuladd  10824  modqmuladdnn0  10826  modaddmodlo  10846  addmodlteq  10856  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdgsuc  10872  frecuzrdgsuctlem  10881  nninfinf  10901  seq3clss  10929  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemab  10960  iseqf1olemmo  10963  iseqf1olemqf1o  10964  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seq3f1olemp  10973  seq3f1oleml  10974  seq3f1o  10975  seqf1oglem1  10977  seqf1oglem2  10978  seqf1og  10979  seq3id3  10982  seqfeq4g  10989  ser3ge0  10994  exp3val  10999  expap0  11027  qsqeqor  11108  modqexp  11125  nn0sqdc  11168  nn0ltexp2  11169  facndiv  11199  faclbnd  11201  bcval5  11223  hashunlem  11266  hashun  11267  hashprg  11271  fiprsshashgt1  11280  hashfacen  11306  hashf1lem1  11307  zfz1isolemiso  11313  zfz1isolem1  11314  seq3coll  11316  hashtpglem  11320  ccatcl  11383  ccatlen  11385  ccatvalfn  11391  ccatsymb  11392  ccatrn  11399  ccat2s1fstg  11438  swrdclg  11444  swrdspsleq  11461  pfxeq  11490  swrdswrd  11499  wrdind  11516  wrd2ind  11517  swrdccatin1  11519  swrdccatin2  11523  pfxccatin12  11527  pfxccat3  11528  swrdccat3b  11534  reuccatpfxs1  11541  ovshftex  11606  2shfti  11618  seq3shft  11625  cjap  11694  caucvgrelemcau  11768  cvg1nlemcau  11772  cvg1nlemres  11773  recvguniq  11783  resqrexlemdecn  11800  resqrexlemcalc3  11804  resqrexlemcvg  11807  resqrexlemoverl  11809  leabs  11862  absexpzap  11869  ltabs  11876  abslt  11877  absle  11878  maxleim  11994  maxabslemval  11997  fimaxre2  12016  fiidxsupcl  12018  minmax  12020  2zinfmin  12034  xrmaxiflemcl  12036  xrmaxifle  12037  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxiflemcom  12040  xrmaxltsup  12049  xrmaxadd  12052  xrminmax  12056  xrbdtri  12067  2clim  12092  climshftlemg  12093  climsqz  12126  climsqz2  12127  climrecvg1n  12139  climcvg1nlem  12140  serf0  12143  sumrbdclem  12169  fsum3cvg  12170  summodclem3  12172  summodclem2a  12173  summodclem2  12174  zsumdc  12176  fsum3  12179  isumss  12183  fisumss  12184  fsum3cvg3  12188  fsumcl2lem  12190  fsumadd  12198  fsumsplit  12199  sumsnf  12201  fsum2d  12227  fisum0diag2  12239  fsummulc2  12240  modfsummod  12250  fsumabs  12257  fsumrelem  12263  fsumiun  12269  geoisumr  12310  cvgratnnlemseq  12318  cvgratz  12324  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  prodrbdclem  12363  fproddccvg  12364  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodntrivap  12376  fprodssdc  12382  fprodmul  12383  prodsnf  12384  fprodsplitdc  12388  fprodsplit  12389  fprodunsn  12396  fprodcl2lem  12397  fprodap0  12413  fprod2d  12415  fprodrec  12421  fprodap0f  12428  efcj  12465  efaddlem  12466  tanaddaplem  12530  sinltxirr  12553  nndivides  12589  dvdsext  12647  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  bitsfzolem  12746  bitsmod  12748  bitsinv1  12754  dvdsbnd  12758  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemzz  12804  bezoutlemaz  12805  bezoutlembz  12806  bezoutlemeu  12809  bezoutlemle  12810  bezoutlemsup  12811  dfgcd3  12812  dfgcd2  12816  bezoutr1  12835  nnmindc  12836  nninfctlemfo  12842  dvdslcm  12872  lcmgcdlem  12880  qredeq  12899  qredeu  12900  divgcdcoprm0  12904  divgcdcoprmex  12905  cncongr1  12906  isprm2lem  12919  prmind2  12923  exprmfct  12942  prmdvdsfz  12943  isprm5lem  12945  prmexpb  12955  rpexp1i  12958  sqrt2irr  12966  pwbdvdslemn  12969  sqne2sq  12982  nonsq  13012  phiprmpw  13029  eulerthlemrprm  13036  eulerthlema  13037  hashgcdeq  13047  phisum  13048  modprmn0modprm0  13064  pclemub  13095  pclemdc  13096  pcmul  13109  pcqmul  13111  pcxqcl  13120  pcdvdstr  13135  pcprmpw2  13141  difsqpwdvds  13146  pcmpt  13151  oddprmdvds  13162  prmpwdvds  13163  pockthg  13165  infpnlem1  13167  1arith  13175  4sqlem2  13197  4sqlemafi  13203  4sqlemffi  13204  4sqleminfi  13205  4sqlem11  13209  4sqlem13m  13211  4sqlem14  13212  4sqlem17  13215  4sqlem18  13216  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemscl  13305  ballotfilemimin  13307  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemsv  13311  ballotfilemsdom  13313  ballotfilemsima  13317  ennnfonelemg  13352  ennnfoneleminc  13360  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemfun  13366  ennnfonelemf1  13367  ennnfonelemrn  13368  ennnfonelemdm  13369  ennnfonelemnn0  13371  ennnfonelemim  13373  exmidunben  13375  ctinfomlemom  13376  ctinf  13379  ctiunctlemudc  13386  nninfdclemlt  13400  nninfdclemf1  13401  isstruct2r  13421  imasival  13686  sgrppropd  13787  mndpropd  13812  issubmnd  13814  mndissubm  13841  resmhm2b  13855  mhmeql  13858  gzsumwsubmcl  13860  gzsumwmhm  13862  gzsumcl  13863  grpinvnz  13935  mhmmnd  13978  mulgfng  13986  mulgz  14012  mulgnndir  14013  mulgnn0dir  14014  mulgneg2  14018  mulgass  14021  mhmmulg  14025  issubgrpd2  14052  issubg4m  14055  grpissubg  14056  isnsg3  14069  ghmpreima  14128  ghmnsgpreima  14131  ghmf1  14135  conjnmz  14141  conjnmzb  14142  cntrsubgnsg  14175  eqgabl  14224  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  gsumvalfi  14242  gsumclfi  14249  gsumf1ofi  14250  gsummptfidmadd  14251  gsumsubmclfi  14253  gsummptfidmsplit  14254  gsumresfi  14263  gsum2dfilem2  14272  prdsval  14280  prdssgrpd  14298  prdsidlem  14300  prdsmndd  14301  pws0g  14320  pwssub  14323  rngpropd  14361  issrg  14376  ringpropd  14450  ringinvnz1ne0  14461  dvdsrvald  14509  dvdsrd  14510  dvdsrtr  14517  unitgrp  14532  rhmopp  14592  aprnzr  14708  opprdrng  14729  lmodfopne  14772  lmodprop2d  14794  lssvacl  14811  lsslss  14827  lss1d  14829  lsspropdg  14877  rnglidlmcl  14926  lidlacl  14930  isridl  14950  gsumfsum  15032  znidomb  15102  znunit  15103  znrrg  15104  issubassa2  15144  psrval  15159  psrbaglefifi  15172  rhmpsrfilem2  15185  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  psrdifi  15202  psrdirfi  15203  mplsubgfilemcl  15215  mplsubgfileminv  15216  mplsubgfi  15217  tgdom  15298  neipsm  15380  tgrest  15395  cnfval  15420  cnpfval  15421  cnpval  15424  iscnp4  15444  cnpnei  15445  cnptopco  15448  cncnpi  15454  cncnp  15456  cnptopresti  15464  cnptoprest2  15466  cndis  15467  lmtopcnp  15476  txbasval  15493  neitx  15494  txcnp  15497  txcnmpt  15499  txcn  15501  imasnopn  15525  psmetres2  15559  isxmet2d  15574  xblss2ps  15630  xblss2  15631  blbas  15659  neibl  15717  metss2lem  15723  metrest  15732  xmettx  15736  metcnp3  15737  metcnp  15738  metcnp2  15739  metcnpi  15741  metcnpi2  15742  mulc1cncf  15815  cncfco  15817  mulcncflem  15833  mulcncf  15834  dedekindeulemuub  15843  dedekindeulemloc  15845  dedekindeulemlu  15847  dedekindeu  15849  suplociccreex  15850  suplociccex  15851  dedekindicclemuub  15852  dedekindicclemloc  15854  dedekindicclemlu  15856  dedekindicclemicc  15858  dedekindicc  15859  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemloc  15867  ivthinc  15869  limcimolemlt  15890  limccnp2lem  15902  limccnp2cntop  15903  limccoap  15904  dvcj  15935  dvmptfsum  15951  dveflem  15952  plyf  15963  plyaddlem1  15973  plymullem1  15974  plycolemc  15984  plyco  15985  plycj  15987  dvply1  15991  dvply2g  15992  efltlemlt  16000  efap1p  16005  sin0pilem1  16008  sin0pilem2  16009  pilem3  16010  coseq0negpitopi  16063  abssinper  16073  cos02pilt1  16079  relogeftb  16094  logdivlt  16124  logbgcd1irraplemexp  16204  logbgcd1irrap  16206  birthdaylem2  16226  ppiqltx  16281  dvdsppwf1o  16283  mpodvdsmulf1o  16284  ppiqub  16293  chtqub  16296  mersenne  16297  perfectlem2  16300  perfect  16301  pcbcctr  16303  bposlem1  16311  bposlem3  16313  bposlem5  16315  lgsval  16328  lgsfvalg  16329  lgsfcl2  16330  lgsval2lem  16334  lgsmod  16350  lgsdilem  16351  lgsdir2lem4  16355  lgsdir2  16357  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem2  16406  2lgslem1a1  16410  2lgslem1a  16412  2sqlem5  16443  2sqlem6  16444  2sqlem7  16445  2sqlem9  16448  2sqlem10  16449  umgrnloopv  16560  uhgr2edg  16652  upgredginwlk  16802  clwwlkccatlem  16846  eupth2lem3lem3fi  16916  eupth2lem3lem4fi  16919  eupth2lemsfi  16924  depindlem3  16954  bj-findis  17210  pwle2  17233  pwf1oexmid  17234  pw1nct  17238  wexmiddiffi  17249  nnsf  17254  peano4nninf  17255  nninfall  17258  nninfsellemeq  17263  nninfsellemeqinf  17265  nnnninfex  17271  nninfnfiinf  17272  qdencn  17278  refeq  17279  trilpolemeq1  17296  trilpolemlt1  17297  trirec0  17300  nconstwlpolemgt0  17321  nconstwlpolem  17322  neapmkvlem  17324