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	|- ( ph -> ps )

Assertion

Ref	Expression
ad2antrr	|- ( ( ( ph /\ ch ) /\ th ) -> ps )

Proof of Theorem ad2antrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantlr 477	1 |- ( ( ( ph /\ ch ) /\ th ) -> ps )

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  1242  vtoclgft  2823  reupick  3457  euotd  4300  frirrg  4398  ralxfrd  4510  nnsucpred  4666  foun  5543  f1oprg  5568  dffo4  5730  funopsn  5764  foeqcnvco  5861  fliftfun  5867  isotr  5887  riotass2  5928  ovmpodxf  6073  mpoxopoveq  6328  tfrlem1  6396  tfrlemibacc  6414  tfrlemibfn  6416  tfrlemi14d  6421  tfrexlem  6422  tfr1onlembacc  6430  tfr1onlembfn  6432  tfr1onlemres  6437  tfrcllembacc  6443  tfrcllembfn  6445  tfrcllemres  6450  frecabcl  6487  nnmordi  6604  eroprf  6717  f1imaen2g  6887  pw2f1odclem  6933  xpen  6944  mapen  6945  mapdom1g  6946  mapxpen  6947  xpmapenlem  6948  phplem4dom  6961  nndomo  6963  phpm  6964  fidifsnen  6969  dif1enen  6979  fisbth  6982  fimax2gtrilemstep  6999  fimax2gtri  7000  en2eqpr  7006  unsnfidcex  7019  unsnfidcel  7020  ssfirab  7035  fidcenumlemrks  7057  sbthlemi8  7068  fiuni  7082  ordiso2  7139  updjud  7186  difinfsnlem  7203  ctssdclemn0  7214  ctssdccl  7215  ctssdc  7217  enumctlemm  7218  enumct  7219  nnnninfeq  7232  nninfisol  7237  enomnilem  7242  fodju0  7251  enmkvlem  7265  enwomnilem  7273  nninfwlpoimlemg  7279  exmidfodomrlemim  7311  exmidontriimlem2  7336  exmidapne  7374  cc3  7382  dfplpq2  7469  nqpi  7493  nqnq0pi  7553  nq0nn  7557  elinp  7589  elnp1st2nd  7591  genprndl  7636  genprndu  7637  addnqprllem  7642  addnqprulem  7643  addnqprl  7644  addnqpru  7645  addlocpr  7651  nqprloc  7660  prmuloc  7681  mulnqprl  7683  mulnqpru  7684  mullocpr  7686  distrlem1prl  7697  distrlem1pru  7698  ltsopr  7711  ltexprlemopl  7716  ltexprlemopu  7718  ltexprlemloc  7722  ltexprlemrl  7725  ltexprlemru  7727  addcanprleml  7729  addcanprlemu  7730  recexprlemloc  7746  recexprlem1ssl  7748  recexprlem1ssu  7749  aptiprleml  7754  aptiprlemu  7755  archpr  7758  cauappcvgprlemm  7760  cauappcvgprlemopl  7761  cauappcvgprlemlol  7762  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  cauappcvgprlemladdru  7771  archrecpr  7779  caucvgprlemnkj  7781  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemlol  7785  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemladdfu  7792  caucvgprprlemnkltj  7804  caucvgprprlemnkeqj  7805  caucvgprprlemnjltk  7806  caucvgprprlemml  7809  caucvgprprlemopl  7812  caucvgprprlemlol  7813  caucvgprprlemdisj  7817  caucvgprprlemexbt  7821  caucvgprprlemexb  7822  caucvgprprlemaddq  7823  suplocexprlemru  7834  suplocexprlemloc  7836  suplocexprlemex  7837  suplocexprlemub  7838  suplocexprlemlub  7839  mulgt0sr  7893  caucvgsrlemcau  7908  caucvgsrlemoffcau  7913  caucvgsrlemoffres  7915  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  axcaucvglemcau  8013  axcaucvglemres  8014  axpre-suploclemres  8016  axsuploc  8147  cnegexlem1  8249  cnegex  8252  apsym  8681  apcotr  8682  apadd1  8683  mulext1  8687  mulge0  8694  apti  8697  aprcl  8721  conjmulap  8804  lemulge11  8941  creui  9035  nndiv  9079  zaddcllemneg  9413  suprzclex  9473  eluzuzle  9658  infregelbex  9721  divfnzn  9744  qapne  9762  xrltso  9920  xnn0dcle  9926  xnn0letri  9927  xrre  9944  xrre3  9946  xaddf  9968  xaddval  9969  xpncan  9995  xleadd1a  9997  xltadd1  10000  xleaddadd  10011  ixxss12  10030  elioc2  10060  elico2  10061  elicc2  10062  fzm1  10224  fzneuz  10225  eluzgtdifelfzo  10328  elfzonelfzo  10361  exfzdc  10371  zsupcllemstep  10374  infssuzex  10378  suprzubdc  10381  nninfdcex  10382  zsupssdc  10383  qtri3or  10385  exbtwnzlemstep  10392  exbtwnzlemex  10394  exbtwnz  10395  modqid  10496  modqcyc2  10507  modqmuladd  10513  modqmuladdnn0  10515  modaddmodlo  10535  addmodlteq  10545  frecuzrdgrrn  10555  frec2uzrdg  10556  frecuzrdgsuc  10561  frecuzrdgsuctlem  10570  nninfinf  10590  seq3clss  10618  iseqf1olemqcl  10646  iseqf1olemnab  10648  iseqf1olemab  10649  iseqf1olemmo  10652  iseqf1olemqf1o  10653  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  seq3f1olemqsumk  10659  seq3f1olemqsum  10660  seq3f1olemp  10662  seq3f1oleml  10663  seq3f1o  10664  seqf1oglem1  10666  seqf1oglem2  10667  seqf1og  10668  seq3id3  10671  seqfeq4g  10678  ser3ge0  10683  exp3val  10688  expap0  10716  qsqeqor  10797  modqexp  10813  nn0ltexp2  10856  facndiv  10886  faclbnd  10888  bcval5  10910  hashunlem  10951  hashun  10952  hashprg  10955  fiprsshashgt1  10964  hashfacen  10983  zfz1isolemiso  10986  zfz1isolem1  10987  seq3coll  10989  ccatcl  11052  ccatlen  11054  ccatvalfn  11060  ccatsymb  11061  ccatrn  11068  swrdclg  11106  swrdspsleq  11123  pfxeq  11150  ovshftex  11163  2shfti  11175  seq3shft  11182  cjap  11250  caucvgrelemcau  11324  cvg1nlemcau  11328  cvg1nlemres  11329  recvguniq  11339  resqrexlemdecn  11356  resqrexlemcalc3  11360  resqrexlemcvg  11363  resqrexlemoverl  11365  leabs  11418  absexpzap  11424  ltabs  11431  abslt  11432  absle  11433  maxleim  11549  maxabslemval  11552  fimaxre2  11571  minmax  11574  2zinfmin  11587  xrmaxiflemcl  11589  xrmaxifle  11590  xrmaxiflemab  11591  xrmaxiflemlub  11592  xrmaxiflemcom  11593  xrmaxltsup  11602  xrmaxadd  11605  xrminmax  11609  xrbdtri  11620  2clim  11645  climshftlemg  11646  climsqz  11679  climsqz2  11680  climrecvg1n  11692  climcvg1nlem  11693  serf0  11696  sumrbdclem  11721  fsum3cvg  11722  summodclem3  11724  summodclem2a  11725  summodclem2  11726  zsumdc  11728  fsum3  11731  isumss  11735  fisumss  11736  fsum3cvg3  11740  fsumcl2lem  11742  fsumadd  11750  fsumsplit  11751  sumsnf  11753  fsum2d  11779  fisum0diag2  11791  fsummulc2  11792  modfsummod  11802  fsumabs  11809  fsumrelem  11815  fsumiun  11821  geoisumr  11862  cvgratnnlemseq  11870  cvgratz  11876  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  prodrbdclem  11915  fproddccvg  11916  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  fprodntrivap  11928  fprodssdc  11934  fprodmul  11935  prodsnf  11936  fprodsplitdc  11940  fprodsplit  11941  fprodunsn  11948  fprodcl2lem  11949  fprodap0  11965  fprod2d  11967  fprodrec  11973  fprodap0f  11980  efcj  12017  efaddlem  12018  tanaddaplem  12082  sinltxirr  12105  nndivides  12141  dvdsext  12199  divalglemeunn  12265  divalglemex  12266  divalglemeuneg  12267  bitsfzolem  12298  bitsmod  12300  bitsinv1  12306  dvdsbnd  12310  bezoutlemnewy  12350  bezoutlemstep  12351  bezoutlemmain  12352  bezoutlemzz  12356  bezoutlemaz  12357  bezoutlembz  12358  bezoutlemeu  12361  bezoutlemle  12362  bezoutlemsup  12363  dfgcd3  12364  dfgcd2  12368  bezoutr1  12387  nnmindc  12388  nninfctlemfo  12394  dvdslcm  12424  lcmgcdlem  12432  qredeq  12451  qredeu  12452  divgcdcoprm0  12456  divgcdcoprmex  12457  cncongr1  12458  isprm2lem  12471  prmind2  12475  exprmfct  12493  prmdvdsfz  12494  isprm5lem  12496  prmexpb  12506  rpexp1i  12509  sqrt2irr  12517  sqne2sq  12532  nonsq  12562  phiprmpw  12577  eulerthlemrprm  12584  eulerthlema  12585  hashgcdeq  12595  phisum  12596  modprmn0modprm0  12612  pclemub  12643  pclemdc  12644  pcmul  12657  pcqmul  12659  pcxqcl  12668  pcdvdstr  12683  pcprmpw2  12689  difsqpwdvds  12694  pcmpt  12699  oddprmdvds  12710  prmpwdvds  12711  pockthg  12713  infpnlem1  12715  1arith  12723  4sqlem2  12745  4sqlemafi  12751  4sqlemffi  12752  4sqleminfi  12753  4sqlem11  12757  4sqlem13m  12759  4sqlem14  12760  4sqlem17  12763  4sqlem18  12764  ennnfonelemg  12807  ennnfoneleminc  12815  ennnfonelemkh  12816  ennnfonelemhf1o  12817  ennnfonelemex  12818  ennnfonelemhom  12819  ennnfonelemfun  12821  ennnfonelemf1  12822  ennnfonelemrn  12823  ennnfonelemdm  12824  ennnfonelemnn0  12826  ennnfonelemim  12828  exmidunben  12830  ctinfomlemom  12831  ctinf  12834  ctiunctlemudc  12841  nninfdclemlt  12855  nninfdclemf1  12856  isstruct2r  12876  prdsval  13138  imasival  13171  gsumpropd2  13258  sgrppropd  13278  prdssgrpd  13280  mndpropd  13305  issubmnd  13307  prdsidlem  13312  prdsmndd  13313  pws0g  13316  mndissubm  13340  resmhm2b  13354  mhmeql  13357  gsumfzz  13360  gsumwsubmcl  13361  gsumwmhm  13363  gsumfzcl  13364  grpinvnz  13436  pwssub  13478  mhmmnd  13485  mulgfng  13493  mulgz  13519  mulgnndir  13520  mulgnn0dir  13521  mulgneg2  13525  mulgass  13528  mhmmulg  13532  issubgrpd2  13559  issubg4m  13562  grpissubg  13563  isnsg3  13576  ghmpreima  13635  ghmnsgpreima  13638  ghmf1  13642  conjnmz  13648  conjnmzb  13649  eqgabl  13699  gsumfzreidx  13706  gsumfzsubmcl  13707  gsumfzmptfidmadd  13708  gsumfzmhm  13712  rngpropd  13750  issrg  13760  ringpropd  13833  ringinvnz1ne0  13844  dvdsrvald  13888  dvdsrd  13889  dvdsrtr  13896  unitgrp  13911  rhmopp  13971  lmodfopne  14121  lmodprop2d  14143  lssvacl  14160  lsslss  14176  lss1d  14178  lsspropdg  14226  rnglidlmcl  14275  lidlacl  14279  isridl  14299  znidomb  14453  znunit  14454  znrrg  14455  psrval  14461  mplsubgfilemcl  14494  mplsubgfileminv  14495  mplsubgfi  14496  tgdom  14577  neipsm  14659  tgrest  14674  cnfval  14699  cnpfval  14700  cnpval  14703  iscnp4  14723  cnpnei  14724  cnptopco  14727  cncnpi  14733  cncnp  14735  cnptopresti  14743  cnptoprest2  14745  cndis  14746  lmtopcnp  14755  txbasval  14772  neitx  14773  txcnp  14776  txcnmpt  14778  txcn  14780  imasnopn  14804  psmetres2  14838  isxmet2d  14853  xblss2ps  14909  xblss2  14910  blbas  14938  neibl  14996  metss2lem  15002  metrest  15011  xmettx  15015  metcnp3  15016  metcnp  15017  metcnp2  15018  metcnpi  15020  metcnpi2  15021  mulc1cncf  15094  cncfco  15096  mulcncflem  15112  mulcncf  15113  dedekindeulemuub  15122  dedekindeulemloc  15124  dedekindeulemlu  15126  dedekindeu  15128  suplociccreex  15129  suplociccex  15130  dedekindicclemuub  15131  dedekindicclemloc  15133  dedekindicclemlu  15135  dedekindicclemicc  15137  dedekindicc  15138  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemloc  15146  ivthinc  15148  limcimolemlt  15169  limccnp2lem  15181  limccnp2cntop  15182  limccoap  15183  dvcj  15214  dvmptfsum  15230  dveflem  15231  plyf  15242  plyaddlem1  15252  plymullem1  15253  plycolemc  15263  plyco  15264  plycj  15266  dvply1  15270  dvply2g  15271  efltlemlt  15279  sin0pilem1  15286  sin0pilem2  15287  pilem3  15288  coseq0negpitopi  15341  abssinper  15351  cos02pilt1  15356  relogeftb  15370  logbgcd1irraplemexp  15473  logbgcd1irrap  15475  dvdsppwf1o  15494  mpodvdsmulf1o  15495  mersenne  15502  perfectlem2  15505  perfect  15506  lgsval  15514  lgsfvalg  15515  lgsfcl2  15516  lgsval2lem  15520  lgsmod  15536  lgsdilem  15537  lgsdir2lem4  15541  lgsdir2  15543  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem2  15592  2lgslem1a1  15596  2lgslem1a  15598  2sqlem5  15629  2sqlem6  15630  2sqlem7  15631  2sqlem9  15634  2sqlem10  15635  bj-findis  15952  2omap  15969  pwle2  15972  pwf1oexmid  15973  pw1nct  15977  nnsf  15979  peano4nninf  15980  nninfall  15983  nninfsellemeq  15988  nninfsellemeqinf  15990  nnnninfex  15996  nninfnfiinf  15997  qdencn  16003  refeq  16004  trilpolemeq1  16016  trilpolemlt1  16017  trirec0  16020  nconstwlpolemgt0  16040  nconstwlpolem  16041  neapmkvlem  16043