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  2852  reupick  3489  euotd  4345  frirrg  4445  ralxfrd  4557  nnsucpred  4713  foun  5599  f1oprg  5625  dffo4  5791  funopsn  5825  foeqcnvco  5926  fliftfun  5932  isotr  5952  riotass2  5995  ovmpodxf  6142  mpoxopoveq  6401  tfrlem1  6469  tfrlemibacc  6487  tfrlemibfn  6489  tfrlemi14d  6494  tfrexlem  6495  tfr1onlembacc  6503  tfr1onlembfn  6505  tfr1onlemres  6510  tfrcllembacc  6516  tfrcllembfn  6518  tfrcllemres  6523  frecabcl  6560  nnmordi  6679  eroprf  6792  f1imaen2g  6962  pw2f1odclem  7015  xpen  7026  mapen  7027  mapdom1g  7028  mapxpen  7029  xpmapenlem  7030  phplem4dom  7043  nndomo  7045  phpm  7047  fidifsnen  7052  dif1enen  7062  fisbth  7065  fimax2gtrilemstep  7083  fimax2gtri  7084  eqsndc  7088  en2eqpr  7092  unsnfidcex  7105  unsnfidcel  7106  ssfirab  7121  fidcenumlemrks  7143  sbthlemi8  7154  fiuni  7168  ordiso2  7225  updjud  7272  difinfsnlem  7289  ctssdclemn0  7300  ctssdccl  7301  ctssdc  7303  enumctlemm  7304  enumct  7305  nnnninfeq  7318  nninfisol  7323  enomnilem  7328  fodju0  7337  enmkvlem  7351  enwomnilem  7359  nninfwlpoimlemg  7365  pr1or2  7390  pr2cv1  7391  exmidfodomrlemim  7402  exmidontriimlem2  7427  exmidapne  7469  cc3  7477  dfplpq2  7564  nqpi  7588  nqnq0pi  7648  nq0nn  7652  elinp  7684  elnp1st2nd  7686  genprndl  7731  genprndu  7732  addnqprllem  7737  addnqprulem  7738  addnqprl  7739  addnqpru  7740  addlocpr  7746  nqprloc  7755  prmuloc  7776  mulnqprl  7778  mulnqpru  7779  mullocpr  7781  distrlem1prl  7792  distrlem1pru  7793  ltsopr  7806  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemloc  7817  ltexprlemrl  7820  ltexprlemru  7822  addcanprleml  7824  addcanprlemu  7825  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  aptiprleml  7849  aptiprlemu  7850  archpr  7853  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlemladdru  7866  archrecpr  7874  caucvgprlemnkj  7876  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemladdfu  7887  caucvgprprlemnkltj  7899  caucvgprprlemnkeqj  7900  caucvgprprlemnjltk  7901  caucvgprprlemml  7904  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemdisj  7912  caucvgprprlemexbt  7916  caucvgprprlemexb  7917  caucvgprprlemaddq  7918  suplocexprlemru  7929  suplocexprlemloc  7931  suplocexprlemex  7932  suplocexprlemub  7933  suplocexprlemlub  7934  mulgt0sr  7988  caucvgsrlemcau  8003  caucvgsrlemoffcau  8008  caucvgsrlemoffres  8010  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  axcaucvglemcau  8108  axcaucvglemres  8109  axpre-suploclemres  8111  axsuploc  8242  cnegexlem1  8344  cnegex  8347  apsym  8776  apcotr  8777  apadd1  8778  mulext1  8782  mulge0  8789  apti  8792  aprcl  8816  conjmulap  8899  lemulge11  9036  creui  9130  nndiv  9174  zaddcllemneg  9508  suprzclex  9568  eluzuzle  9754  infregelbex  9822  divfnzn  9845  qapne  9863  xrltso  10021  xnn0dcle  10027  xnn0letri  10028  xrre  10045  xrre3  10047  xaddf  10069  xaddval  10070  xpncan  10096  xleadd1a  10098  xltadd1  10101  xleaddadd  10112  ixxss12  10131  elioc2  10161  elico2  10162  elicc2  10163  fzm1  10325  fzneuz  10326  eluzgtdifelfzo  10432  elfzonelfzo  10465  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  suprzubdc  10486  nninfdcex  10487  zsupssdc  10488  qtri3or  10490  exbtwnzlemstep  10497  exbtwnzlemex  10499  exbtwnz  10500  modqid  10601  modqcyc2  10612  modqmuladd  10618  modqmuladdnn0  10620  modaddmodlo  10640  addmodlteq  10650  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdgsuc  10666  frecuzrdgsuctlem  10675  nninfinf  10695  seq3clss  10723  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemab  10754  iseqf1olemmo  10757  iseqf1olemqf1o  10758  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seq3f1olemp  10767  seq3f1oleml  10768  seq3f1o  10769  seqf1oglem1  10771  seqf1oglem2  10772  seqf1og  10773  seq3id3  10776  seqfeq4g  10783  ser3ge0  10788  exp3val  10793  expap0  10821  qsqeqor  10902  modqexp  10918  nn0ltexp2  10961  facndiv  10991  faclbnd  10993  bcval5  11015  hashunlem  11057  hashun  11058  hashprg  11062  fiprsshashgt1  11071  hashfacen  11090  zfz1isolemiso  11093  zfz1isolem1  11094  seq3coll  11096  ccatcl  11160  ccatlen  11162  ccatvalfn  11168  ccatsymb  11169  ccatrn  11176  ccat2s1fstg  11215  swrdclg  11221  swrdspsleq  11238  pfxeq  11267  swrdswrd  11276  wrdind  11293  wrd2ind  11294  swrdccatin1  11296  swrdccatin2  11300  pfxccatin12  11304  pfxccat3  11305  swrdccat3b  11311  reuccatpfxs1  11318  ovshftex  11370  2shfti  11382  seq3shft  11389  cjap  11457  caucvgrelemcau  11531  cvg1nlemcau  11535  cvg1nlemres  11536  recvguniq  11546  resqrexlemdecn  11563  resqrexlemcalc3  11567  resqrexlemcvg  11570  resqrexlemoverl  11572  leabs  11625  absexpzap  11631  ltabs  11638  abslt  11639  absle  11640  maxleim  11756  maxabslemval  11759  fimaxre2  11778  minmax  11781  2zinfmin  11794  xrmaxiflemcl  11796  xrmaxifle  11797  xrmaxiflemab  11798  xrmaxiflemlub  11799  xrmaxiflemcom  11800  xrmaxltsup  11809  xrmaxadd  11812  xrminmax  11816  xrbdtri  11827  2clim  11852  climshftlemg  11853  climsqz  11886  climsqz2  11887  climrecvg1n  11899  climcvg1nlem  11900  serf0  11903  sumrbdclem  11928  fsum3cvg  11929  summodclem3  11931  summodclem2a  11932  summodclem2  11933  zsumdc  11935  fsum3  11938  isumss  11942  fisumss  11943  fsum3cvg3  11947  fsumcl2lem  11949  fsumadd  11957  fsumsplit  11958  sumsnf  11960  fsum2d  11986  fisum0diag2  11998  fsummulc2  11999  modfsummod  12009  fsumabs  12016  fsumrelem  12022  fsumiun  12028  geoisumr  12069  cvgratnnlemseq  12077  cvgratz  12083  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  prodrbdclem  12122  fproddccvg  12123  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  fprodntrivap  12135  fprodssdc  12141  fprodmul  12142  prodsnf  12143  fprodsplitdc  12147  fprodsplit  12148  fprodunsn  12155  fprodcl2lem  12156  fprodap0  12172  fprod2d  12174  fprodrec  12180  fprodap0f  12187  efcj  12224  efaddlem  12225  tanaddaplem  12289  sinltxirr  12312  nndivides  12348  dvdsext  12406  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  bitsfzolem  12505  bitsmod  12507  bitsinv1  12513  dvdsbnd  12517  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlemmain  12559  bezoutlemzz  12563  bezoutlemaz  12564  bezoutlembz  12565  bezoutlemeu  12568  bezoutlemle  12569  bezoutlemsup  12570  dfgcd3  12571  dfgcd2  12575  bezoutr1  12594  nnmindc  12595  nninfctlemfo  12601  dvdslcm  12631  lcmgcdlem  12639  qredeq  12658  qredeu  12659  divgcdcoprm0  12663  divgcdcoprmex  12664  cncongr1  12665  isprm2lem  12678  prmind2  12682  exprmfct  12700  prmdvdsfz  12701  isprm5lem  12703  prmexpb  12713  rpexp1i  12716  sqrt2irr  12724  sqne2sq  12739  nonsq  12769  phiprmpw  12784  eulerthlemrprm  12791  eulerthlema  12792  hashgcdeq  12802  phisum  12803  modprmn0modprm0  12819  pclemub  12850  pclemdc  12851  pcmul  12864  pcqmul  12866  pcxqcl  12875  pcdvdstr  12890  pcprmpw2  12896  difsqpwdvds  12901  pcmpt  12906  oddprmdvds  12917  prmpwdvds  12918  pockthg  12920  infpnlem1  12922  1arith  12930  4sqlem2  12952  4sqlemafi  12958  4sqlemffi  12959  4sqleminfi  12960  4sqlem11  12964  4sqlem13m  12966  4sqlem14  12967  4sqlem17  12970  4sqlem18  12971  ennnfonelemg  13014  ennnfoneleminc  13022  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemfun  13028  ennnfonelemf1  13029  ennnfonelemrn  13030  ennnfonelemdm  13031  ennnfonelemnn0  13033  ennnfonelemim  13035  exmidunben  13037  ctinfomlemom  13038  ctinf  13041  ctiunctlemudc  13048  nninfdclemlt  13062  nninfdclemf1  13063  isstruct2r  13083  prdsval  13346  imasival  13379  gsumpropd2  13466  sgrppropd  13486  prdssgrpd  13488  mndpropd  13513  issubmnd  13515  prdsidlem  13520  prdsmndd  13521  pws0g  13524  mndissubm  13548  resmhm2b  13562  mhmeql  13565  gsumfzz  13568  gsumwsubmcl  13569  gsumwmhm  13571  gsumfzcl  13572  grpinvnz  13644  pwssub  13686  mhmmnd  13693  mulgfng  13701  mulgz  13727  mulgnndir  13728  mulgnn0dir  13729  mulgneg2  13733  mulgass  13736  mhmmulg  13740  issubgrpd2  13767  issubg4m  13770  grpissubg  13771  isnsg3  13784  ghmpreima  13843  ghmnsgpreima  13846  ghmf1  13850  conjnmz  13856  conjnmzb  13857  eqgabl  13907  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  rngpropd  13958  issrg  13968  ringpropd  14041  ringinvnz1ne0  14052  dvdsrvald  14097  dvdsrd  14098  dvdsrtr  14105  unitgrp  14120  rhmopp  14180  lmodfopne  14330  lmodprop2d  14352  lssvacl  14369  lsslss  14385  lss1d  14387  lsspropdg  14435  rnglidlmcl  14484  lidlacl  14488  isridl  14508  znidomb  14662  znunit  14663  znrrg  14664  psrval  14670  mplsubgfilemcl  14703  mplsubgfileminv  14704  mplsubgfi  14705  tgdom  14786  neipsm  14868  tgrest  14883  cnfval  14908  cnpfval  14909  cnpval  14912  iscnp4  14932  cnpnei  14933  cnptopco  14936  cncnpi  14942  cncnp  14944  cnptopresti  14952  cnptoprest2  14954  cndis  14955  lmtopcnp  14964  txbasval  14981  neitx  14982  txcnp  14985  txcnmpt  14987  txcn  14989  imasnopn  15013  psmetres2  15047  isxmet2d  15062  xblss2ps  15118  xblss2  15119  blbas  15147  neibl  15205  metss2lem  15211  metrest  15220  xmettx  15224  metcnp3  15225  metcnp  15226  metcnp2  15227  metcnpi  15229  metcnpi2  15230  mulc1cncf  15303  cncfco  15305  mulcncflem  15321  mulcncf  15322  dedekindeulemuub  15331  dedekindeulemloc  15333  dedekindeulemlu  15335  dedekindeu  15337  suplociccreex  15338  suplociccex  15339  dedekindicclemuub  15340  dedekindicclemloc  15342  dedekindicclemlu  15344  dedekindicclemicc  15346  dedekindicc  15347  ivthinclemlopn  15350  ivthinclemlr  15351  ivthinclemuopn  15352  ivthinclemur  15353  ivthinclemloc  15355  ivthinc  15357  limcimolemlt  15378  limccnp2lem  15390  limccnp2cntop  15391  limccoap  15392  dvcj  15423  dvmptfsum  15439  dveflem  15440  plyf  15451  plyaddlem1  15461  plymullem1  15462  plycolemc  15472  plyco  15473  plycj  15475  dvply1  15479  dvply2g  15480  efltlemlt  15488  sin0pilem1  15495  sin0pilem2  15496  pilem3  15497  coseq0negpitopi  15550  abssinper  15560  cos02pilt1  15565  relogeftb  15579  logbgcd1irraplemexp  15682  logbgcd1irrap  15684  dvdsppwf1o  15703  mpodvdsmulf1o  15704  mersenne  15711  perfectlem2  15714  perfect  15715  lgsval  15723  lgsfvalg  15724  lgsfcl2  15725  lgsval2lem  15729  lgsmod  15745  lgsdilem  15746  lgsdir2lem4  15750  lgsdir2  15752  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem2  15801  2lgslem1a1  15805  2lgslem1a  15807  2sqlem5  15838  2sqlem6  15839  2sqlem7  15840  2sqlem9  15843  2sqlem10  15844  umgrnloopv  15955  uhgr2edg  16045  upgredginwlk  16153  clwwlkccatlem  16195  bj-findis  16510  2omap  16530  pwle2  16535  pwf1oexmid  16536  pw1nct  16540  nnsf  16543  peano4nninf  16544  nninfall  16547  nninfsellemeq  16552  nninfsellemeqinf  16554  nnnninfex  16560  nninfnfiinf  16561  qdencn  16567  refeq  16568  trilpolemeq1  16580  trilpolemlt1  16581  trirec0  16584  nconstwlpolemgt0  16604  nconstwlpolem  16605  neapmkvlem  16607