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  2828  reupick  3465  euotd  4317  frirrg  4415  ralxfrd  4527  nnsucpred  4683  foun  5563  f1oprg  5589  dffo4  5751  funopsn  5785  foeqcnvco  5882  fliftfun  5888  isotr  5908  riotass2  5949  ovmpodxf  6094  mpoxopoveq  6349  tfrlem1  6417  tfrlemibacc  6435  tfrlemibfn  6437  tfrlemi14d  6442  tfrexlem  6443  tfr1onlembacc  6451  tfr1onlembfn  6453  tfr1onlemres  6458  tfrcllembacc  6464  tfrcllembfn  6466  tfrcllemres  6471  frecabcl  6508  nnmordi  6625  eroprf  6738  f1imaen2g  6908  pw2f1odclem  6956  xpen  6967  mapen  6968  mapdom1g  6969  mapxpen  6970  xpmapenlem  6971  phplem4dom  6984  nndomo  6986  phpm  6988  fidifsnen  6993  dif1enen  7003  fisbth  7006  fimax2gtrilemstep  7023  fimax2gtri  7024  en2eqpr  7030  unsnfidcex  7043  unsnfidcel  7044  ssfirab  7059  fidcenumlemrks  7081  sbthlemi8  7092  fiuni  7106  ordiso2  7163  updjud  7210  difinfsnlem  7227  ctssdclemn0  7238  ctssdccl  7239  ctssdc  7241  enumctlemm  7242  enumct  7243  nnnninfeq  7256  nninfisol  7261  enomnilem  7266  fodju0  7275  enmkvlem  7289  enwomnilem  7297  nninfwlpoimlemg  7303  pr1or2  7328  pr2cv1  7329  exmidfodomrlemim  7340  exmidontriimlem2  7365  exmidapne  7407  cc3  7415  dfplpq2  7502  nqpi  7526  nqnq0pi  7586  nq0nn  7590  elinp  7622  elnp1st2nd  7624  genprndl  7669  genprndu  7670  addnqprllem  7675  addnqprulem  7676  addnqprl  7677  addnqpru  7678  addlocpr  7684  nqprloc  7693  prmuloc  7714  mulnqprl  7716  mulnqpru  7717  mullocpr  7719  distrlem1prl  7730  distrlem1pru  7731  ltsopr  7744  ltexprlemopl  7749  ltexprlemopu  7751  ltexprlemloc  7755  ltexprlemrl  7758  ltexprlemru  7760  addcanprleml  7762  addcanprlemu  7763  recexprlemloc  7779  recexprlem1ssl  7781  recexprlem1ssu  7782  aptiprleml  7787  aptiprlemu  7788  archpr  7791  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  cauappcvgprlemladdru  7804  archrecpr  7812  caucvgprlemnkj  7814  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemladdfu  7825  caucvgprprlemnkltj  7837  caucvgprprlemnkeqj  7838  caucvgprprlemnjltk  7839  caucvgprprlemml  7842  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemdisj  7850  caucvgprprlemexbt  7854  caucvgprprlemexb  7855  caucvgprprlemaddq  7856  suplocexprlemru  7867  suplocexprlemloc  7869  suplocexprlemex  7870  suplocexprlemub  7871  suplocexprlemlub  7872  mulgt0sr  7926  caucvgsrlemcau  7941  caucvgsrlemoffcau  7946  caucvgsrlemoffres  7948  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  axcaucvglemcau  8046  axcaucvglemres  8047  axpre-suploclemres  8049  axsuploc  8180  cnegexlem1  8282  cnegex  8285  apsym  8714  apcotr  8715  apadd1  8716  mulext1  8720  mulge0  8727  apti  8730  aprcl  8754  conjmulap  8837  lemulge11  8974  creui  9068  nndiv  9112  zaddcllemneg  9446  suprzclex  9506  eluzuzle  9691  infregelbex  9754  divfnzn  9777  qapne  9795  xrltso  9953  xnn0dcle  9959  xnn0letri  9960  xrre  9977  xrre3  9979  xaddf  10001  xaddval  10002  xpncan  10028  xleadd1a  10030  xltadd1  10033  xleaddadd  10044  ixxss12  10063  elioc2  10093  elico2  10094  elicc2  10095  fzm1  10257  fzneuz  10258  eluzgtdifelfzo  10363  elfzonelfzo  10396  exfzdc  10406  zsupcllemstep  10409  infssuzex  10413  suprzubdc  10416  nninfdcex  10417  zsupssdc  10418  qtri3or  10420  exbtwnzlemstep  10427  exbtwnzlemex  10429  exbtwnz  10430  modqid  10531  modqcyc2  10542  modqmuladd  10548  modqmuladdnn0  10550  modaddmodlo  10570  addmodlteq  10580  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgsuc  10596  frecuzrdgsuctlem  10605  nninfinf  10625  seq3clss  10653  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemab  10684  iseqf1olemmo  10687  iseqf1olemqf1o  10688  iseqf1olemjpcl  10690  iseqf1olemqpcl  10691  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  seq3f1olemp  10697  seq3f1oleml  10698  seq3f1o  10699  seqf1oglem1  10701  seqf1oglem2  10702  seqf1og  10703  seq3id3  10706  seqfeq4g  10713  ser3ge0  10718  exp3val  10723  expap0  10751  qsqeqor  10832  modqexp  10848  nn0ltexp2  10891  facndiv  10921  faclbnd  10923  bcval5  10945  hashunlem  10986  hashun  10987  hashprg  10990  fiprsshashgt1  10999  hashfacen  11018  zfz1isolemiso  11021  zfz1isolem1  11022  seq3coll  11024  ccatcl  11087  ccatlen  11089  ccatvalfn  11095  ccatsymb  11096  ccatrn  11103  swrdclg  11141  swrdspsleq  11158  pfxeq  11187  swrdswrd  11196  wrdind  11213  wrd2ind  11214  swrdccatin1  11216  swrdccatin2  11220  pfxccatin12  11224  pfxccat3  11225  swrdccat3b  11231  reuccatpfxs1  11238  ovshftex  11245  2shfti  11257  seq3shft  11264  cjap  11332  caucvgrelemcau  11406  cvg1nlemcau  11410  cvg1nlemres  11411  recvguniq  11421  resqrexlemdecn  11438  resqrexlemcalc3  11442  resqrexlemcvg  11445  resqrexlemoverl  11447  leabs  11500  absexpzap  11506  ltabs  11513  abslt  11514  absle  11515  maxleim  11631  maxabslemval  11634  fimaxre2  11653  minmax  11656  2zinfmin  11669  xrmaxiflemcl  11671  xrmaxifle  11672  xrmaxiflemab  11673  xrmaxiflemlub  11674  xrmaxiflemcom  11675  xrmaxltsup  11684  xrmaxadd  11687  xrminmax  11691  xrbdtri  11702  2clim  11727  climshftlemg  11728  climsqz  11761  climsqz2  11762  climrecvg1n  11774  climcvg1nlem  11775  serf0  11778  sumrbdclem  11803  fsum3cvg  11804  summodclem3  11806  summodclem2a  11807  summodclem2  11808  zsumdc  11810  fsum3  11813  isumss  11817  fisumss  11818  fsum3cvg3  11822  fsumcl2lem  11824  fsumadd  11832  fsumsplit  11833  sumsnf  11835  fsum2d  11861  fisum0diag2  11873  fsummulc2  11874  modfsummod  11884  fsumabs  11891  fsumrelem  11897  fsumiun  11903  geoisumr  11944  cvgratnnlemseq  11952  cvgratz  11958  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  prodrbdclem  11997  fproddccvg  11998  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  fprodntrivap  12010  fprodssdc  12016  fprodmul  12017  prodsnf  12018  fprodsplitdc  12022  fprodsplit  12023  fprodunsn  12030  fprodcl2lem  12031  fprodap0  12047  fprod2d  12049  fprodrec  12055  fprodap0f  12062  efcj  12099  efaddlem  12100  tanaddaplem  12164  sinltxirr  12187  nndivides  12223  dvdsext  12281  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  bitsfzolem  12380  bitsmod  12382  bitsinv1  12388  dvdsbnd  12392  bezoutlemnewy  12432  bezoutlemstep  12433  bezoutlemmain  12434  bezoutlemzz  12438  bezoutlemaz  12439  bezoutlembz  12440  bezoutlemeu  12443  bezoutlemle  12444  bezoutlemsup  12445  dfgcd3  12446  dfgcd2  12450  bezoutr1  12469  nnmindc  12470  nninfctlemfo  12476  dvdslcm  12506  lcmgcdlem  12514  qredeq  12533  qredeu  12534  divgcdcoprm0  12538  divgcdcoprmex  12539  cncongr1  12540  isprm2lem  12553  prmind2  12557  exprmfct  12575  prmdvdsfz  12576  isprm5lem  12578  prmexpb  12588  rpexp1i  12591  sqrt2irr  12599  sqne2sq  12614  nonsq  12644  phiprmpw  12659  eulerthlemrprm  12666  eulerthlema  12667  hashgcdeq  12677  phisum  12678  modprmn0modprm0  12694  pclemub  12725  pclemdc  12726  pcmul  12739  pcqmul  12741  pcxqcl  12750  pcdvdstr  12765  pcprmpw2  12771  difsqpwdvds  12776  pcmpt  12781  oddprmdvds  12792  prmpwdvds  12793  pockthg  12795  infpnlem1  12797  1arith  12805  4sqlem2  12827  4sqlemafi  12833  4sqlemffi  12834  4sqleminfi  12835  4sqlem11  12839  4sqlem13m  12841  4sqlem14  12842  4sqlem17  12845  4sqlem18  12846  ennnfonelemg  12889  ennnfoneleminc  12897  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemfun  12903  ennnfonelemf1  12904  ennnfonelemrn  12905  ennnfonelemdm  12906  ennnfonelemnn0  12908  ennnfonelemim  12910  exmidunben  12912  ctinfomlemom  12913  ctinf  12916  ctiunctlemudc  12923  nninfdclemlt  12937  nninfdclemf1  12938  isstruct2r  12958  prdsval  13220  imasival  13253  gsumpropd2  13340  sgrppropd  13360  prdssgrpd  13362  mndpropd  13387  issubmnd  13389  prdsidlem  13394  prdsmndd  13395  pws0g  13398  mndissubm  13422  resmhm2b  13436  mhmeql  13439  gsumfzz  13442  gsumwsubmcl  13443  gsumwmhm  13445  gsumfzcl  13446  grpinvnz  13518  pwssub  13560  mhmmnd  13567  mulgfng  13575  mulgz  13601  mulgnndir  13602  mulgnn0dir  13603  mulgneg2  13607  mulgass  13610  mhmmulg  13614  issubgrpd2  13641  issubg4m  13644  grpissubg  13645  isnsg3  13658  ghmpreima  13717  ghmnsgpreima  13720  ghmf1  13724  conjnmz  13730  conjnmzb  13731  eqgabl  13781  gsumfzreidx  13788  gsumfzsubmcl  13789  gsumfzmptfidmadd  13790  gsumfzmhm  13794  rngpropd  13832  issrg  13842  ringpropd  13915  ringinvnz1ne0  13926  dvdsrvald  13970  dvdsrd  13971  dvdsrtr  13978  unitgrp  13993  rhmopp  14053  lmodfopne  14203  lmodprop2d  14225  lssvacl  14242  lsslss  14258  lss1d  14260  lsspropdg  14308  rnglidlmcl  14357  lidlacl  14361  isridl  14381  znidomb  14535  znunit  14536  znrrg  14537  psrval  14543  mplsubgfilemcl  14576  mplsubgfileminv  14577  mplsubgfi  14578  tgdom  14659  neipsm  14741  tgrest  14756  cnfval  14781  cnpfval  14782  cnpval  14785  iscnp4  14805  cnpnei  14806  cnptopco  14809  cncnpi  14815  cncnp  14817  cnptopresti  14825  cnptoprest2  14827  cndis  14828  lmtopcnp  14837  txbasval  14854  neitx  14855  txcnp  14858  txcnmpt  14860  txcn  14862  imasnopn  14886  psmetres2  14920  isxmet2d  14935  xblss2ps  14991  xblss2  14992  blbas  15020  neibl  15078  metss2lem  15084  metrest  15093  xmettx  15097  metcnp3  15098  metcnp  15099  metcnp2  15100  metcnpi  15102  metcnpi2  15103  mulc1cncf  15176  cncfco  15178  mulcncflem  15194  mulcncf  15195  dedekindeulemuub  15204  dedekindeulemloc  15206  dedekindeulemlu  15208  dedekindeu  15210  suplociccreex  15211  suplociccex  15212  dedekindicclemuub  15213  dedekindicclemloc  15215  dedekindicclemlu  15217  dedekindicclemicc  15219  dedekindicc  15220  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemloc  15228  ivthinc  15230  limcimolemlt  15251  limccnp2lem  15263  limccnp2cntop  15264  limccoap  15265  dvcj  15296  dvmptfsum  15312  dveflem  15313  plyf  15324  plyaddlem1  15334  plymullem1  15335  plycolemc  15345  plyco  15346  plycj  15348  dvply1  15352  dvply2g  15353  efltlemlt  15361  sin0pilem1  15368  sin0pilem2  15369  pilem3  15370  coseq0negpitopi  15423  abssinper  15433  cos02pilt1  15438  relogeftb  15452  logbgcd1irraplemexp  15555  logbgcd1irrap  15557  dvdsppwf1o  15576  mpodvdsmulf1o  15577  mersenne  15584  perfectlem2  15587  perfect  15588  lgsval  15596  lgsfvalg  15597  lgsfcl2  15598  lgsval2lem  15602  lgsmod  15618  lgsdilem  15619  lgsdir2lem4  15623  lgsdir2  15625  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem2  15674  2lgslem1a1  15678  2lgslem1a  15680  2sqlem5  15711  2sqlem6  15712  2sqlem7  15713  2sqlem9  15716  2sqlem10  15717  umgrnloopvv  15825  bj-findis  16114  2omap  16132  pwle2  16137  pwf1oexmid  16138  pw1nct  16142  nnsf  16144  peano4nninf  16145  nninfall  16148  nninfsellemeq  16153  nninfsellemeqinf  16155  nnnninfex  16161  nninfnfiinf  16162  qdencn  16168  refeq  16169  trilpolemeq1  16181  trilpolemlt1  16182  trirec0  16185  nconstwlpolemgt0  16205  nconstwlpolem  16206  neapmkvlem  16208