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  4299  frirrg  4397  ralxfrd  4509  nnsucpred  4665  foun  5541  f1oprg  5566  dffo4  5728  funopsn  5762  foeqcnvco  5859  fliftfun  5865  isotr  5885  riotass2  5926  ovmpodxf  6071  mpoxopoveq  6326  tfrlem1  6394  tfrlemibacc  6412  tfrlemibfn  6414  tfrlemi14d  6419  tfrexlem  6420  tfr1onlembacc  6428  tfr1onlembfn  6430  tfr1onlemres  6435  tfrcllembacc  6441  tfrcllembfn  6443  tfrcllemres  6448  frecabcl  6485  nnmordi  6602  eroprf  6715  f1imaen2g  6885  pw2f1odclem  6931  xpen  6942  mapen  6943  mapdom1g  6944  mapxpen  6945  xpmapenlem  6946  phplem4dom  6959  nndomo  6961  phpm  6962  fidifsnen  6967  dif1enen  6977  fisbth  6980  fimax2gtrilemstep  6997  fimax2gtri  6998  en2eqpr  7004  unsnfidcex  7017  unsnfidcel  7018  ssfirab  7033  fidcenumlemrks  7055  sbthlemi8  7066  fiuni  7080  ordiso2  7137  updjud  7184  difinfsnlem  7201  ctssdclemn0  7212  ctssdccl  7213  ctssdc  7215  enumctlemm  7216  enumct  7217  nnnninfeq  7230  nninfisol  7235  enomnilem  7240  fodju0  7249  enmkvlem  7263  enwomnilem  7271  nninfwlpoimlemg  7277  exmidfodomrlemim  7309  exmidontriimlem2  7334  exmidapne  7372  cc3  7380  dfplpq2  7467  nqpi  7491  nqnq0pi  7551  nq0nn  7555  elinp  7587  elnp1st2nd  7589  genprndl  7634  genprndu  7635  addnqprllem  7640  addnqprulem  7641  addnqprl  7642  addnqpru  7643  addlocpr  7649  nqprloc  7658  prmuloc  7679  mulnqprl  7681  mulnqpru  7682  mullocpr  7684  distrlem1prl  7695  distrlem1pru  7696  ltsopr  7709  ltexprlemopl  7714  ltexprlemopu  7716  ltexprlemloc  7720  ltexprlemrl  7723  ltexprlemru  7725  addcanprleml  7727  addcanprlemu  7728  recexprlemloc  7744  recexprlem1ssl  7746  recexprlem1ssu  7747  aptiprleml  7752  aptiprlemu  7753  archpr  7756  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  cauappcvgprlemladdru  7769  archrecpr  7777  caucvgprlemnkj  7779  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemladdfu  7790  caucvgprprlemnkltj  7802  caucvgprprlemnkeqj  7803  caucvgprprlemnjltk  7804  caucvgprprlemml  7807  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemdisj  7815  caucvgprprlemexbt  7819  caucvgprprlemexb  7820  caucvgprprlemaddq  7821  suplocexprlemru  7832  suplocexprlemloc  7834  suplocexprlemex  7835  suplocexprlemub  7836  suplocexprlemlub  7837  mulgt0sr  7891  caucvgsrlemcau  7906  caucvgsrlemoffcau  7911  caucvgsrlemoffres  7913  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  axcaucvglemcau  8011  axcaucvglemres  8012  axpre-suploclemres  8014  axsuploc  8145  cnegexlem1  8247  cnegex  8250  apsym  8679  apcotr  8680  apadd1  8681  mulext1  8685  mulge0  8692  apti  8695  aprcl  8719  conjmulap  8802  lemulge11  8939  creui  9033  nndiv  9077  zaddcllemneg  9411  suprzclex  9471  eluzuzle  9656  infregelbex  9719  divfnzn  9742  qapne  9760  xrltso  9918  xnn0dcle  9924  xnn0letri  9925  xrre  9942  xrre3  9944  xaddf  9966  xaddval  9967  xpncan  9993  xleadd1a  9995  xltadd1  9998  xleaddadd  10009  ixxss12  10028  elioc2  10058  elico2  10059  elicc2  10060  fzm1  10222  fzneuz  10223  eluzgtdifelfzo  10326  elfzonelfzo  10359  exfzdc  10369  zsupcllemstep  10372  infssuzex  10376  suprzubdc  10379  nninfdcex  10380  zsupssdc  10381  qtri3or  10383  exbtwnzlemstep  10390  exbtwnzlemex  10392  exbtwnz  10393  modqid  10494  modqcyc2  10505  modqmuladd  10511  modqmuladdnn0  10513  modaddmodlo  10533  addmodlteq  10543  frecuzrdgrrn  10553  frec2uzrdg  10554  frecuzrdgsuc  10559  frecuzrdgsuctlem  10568  nninfinf  10588  seq3clss  10616  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemab  10647  iseqf1olemmo  10650  iseqf1olemqf1o  10651  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  seq3f1olemqsumk  10657  seq3f1olemqsum  10658  seq3f1olemp  10660  seq3f1oleml  10661  seq3f1o  10662  seqf1oglem1  10664  seqf1oglem2  10665  seqf1og  10666  seq3id3  10669  seqfeq4g  10676  ser3ge0  10681  exp3val  10686  expap0  10714  qsqeqor  10795  modqexp  10811  nn0ltexp2  10854  facndiv  10884  faclbnd  10886  bcval5  10908  hashunlem  10949  hashun  10950  hashprg  10953  fiprsshashgt1  10962  hashfacen  10981  zfz1isolemiso  10984  zfz1isolem1  10985  seq3coll  10987  ccatcl  11049  ccatlen  11051  ccatvalfn  11057  ccatsymb  11058  ccatrn  11065  swrdclg  11103  swrdspsleq  11120  ovshftex  11130  2shfti  11142  seq3shft  11149  cjap  11217  caucvgrelemcau  11291  cvg1nlemcau  11295  cvg1nlemres  11296  recvguniq  11306  resqrexlemdecn  11323  resqrexlemcalc3  11327  resqrexlemcvg  11330  resqrexlemoverl  11332  leabs  11385  absexpzap  11391  ltabs  11398  abslt  11399  absle  11400  maxleim  11516  maxabslemval  11519  fimaxre2  11538  minmax  11541  2zinfmin  11554  xrmaxiflemcl  11556  xrmaxifle  11557  xrmaxiflemab  11558  xrmaxiflemlub  11559  xrmaxiflemcom  11560  xrmaxltsup  11569  xrmaxadd  11572  xrminmax  11576  xrbdtri  11587  2clim  11612  climshftlemg  11613  climsqz  11646  climsqz2  11647  climrecvg1n  11659  climcvg1nlem  11660  serf0  11663  sumrbdclem  11688  fsum3cvg  11689  summodclem3  11691  summodclem2a  11692  summodclem2  11693  zsumdc  11695  fsum3  11698  isumss  11702  fisumss  11703  fsum3cvg3  11707  fsumcl2lem  11709  fsumadd  11717  fsumsplit  11718  sumsnf  11720  fsum2d  11746  fisum0diag2  11758  fsummulc2  11759  modfsummod  11769  fsumabs  11776  fsumrelem  11782  fsumiun  11788  geoisumr  11829  cvgratnnlemseq  11837  cvgratz  11843  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  prodrbdclem  11882  fproddccvg  11883  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodntrivap  11895  fprodssdc  11901  fprodmul  11902  prodsnf  11903  fprodsplitdc  11907  fprodsplit  11908  fprodunsn  11915  fprodcl2lem  11916  fprodap0  11932  fprod2d  11934  fprodrec  11940  fprodap0f  11947  efcj  11984  efaddlem  11985  tanaddaplem  12049  sinltxirr  12072  nndivides  12108  dvdsext  12166  divalglemeunn  12232  divalglemex  12233  divalglemeuneg  12234  bitsfzolem  12265  bitsmod  12267  bitsinv1  12273  dvdsbnd  12277  bezoutlemnewy  12317  bezoutlemstep  12318  bezoutlemmain  12319  bezoutlemzz  12323  bezoutlemaz  12324  bezoutlembz  12325  bezoutlemeu  12328  bezoutlemle  12329  bezoutlemsup  12330  dfgcd3  12331  dfgcd2  12335  bezoutr1  12354  nnmindc  12355  nninfctlemfo  12361  dvdslcm  12391  lcmgcdlem  12399  qredeq  12418  qredeu  12419  divgcdcoprm0  12423  divgcdcoprmex  12424  cncongr1  12425  isprm2lem  12438  prmind2  12442  exprmfct  12460  prmdvdsfz  12461  isprm5lem  12463  prmexpb  12473  rpexp1i  12476  sqrt2irr  12484  sqne2sq  12499  nonsq  12529  phiprmpw  12544  eulerthlemrprm  12551  eulerthlema  12552  hashgcdeq  12562  phisum  12563  modprmn0modprm0  12579  pclemub  12610  pclemdc  12611  pcmul  12624  pcqmul  12626  pcxqcl  12635  pcdvdstr  12650  pcprmpw2  12656  difsqpwdvds  12661  pcmpt  12666  oddprmdvds  12677  prmpwdvds  12678  pockthg  12680  infpnlem1  12682  1arith  12690  4sqlem2  12712  4sqlemafi  12718  4sqlemffi  12719  4sqleminfi  12720  4sqlem11  12724  4sqlem13m  12726  4sqlem14  12727  4sqlem17  12730  4sqlem18  12731  ennnfonelemg  12774  ennnfoneleminc  12782  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemfun  12788  ennnfonelemf1  12789  ennnfonelemrn  12790  ennnfonelemdm  12791  ennnfonelemnn0  12793  ennnfonelemim  12795  exmidunben  12797  ctinfomlemom  12798  ctinf  12801  ctiunctlemudc  12808  nninfdclemlt  12822  nninfdclemf1  12823  isstruct2r  12843  prdsval  13105  imasival  13138  gsumpropd2  13225  sgrppropd  13245  prdssgrpd  13247  mndpropd  13272  issubmnd  13274  prdsidlem  13279  prdsmndd  13280  pws0g  13283  mndissubm  13307  resmhm2b  13321  mhmeql  13324  gsumfzz  13327  gsumwsubmcl  13328  gsumwmhm  13330  gsumfzcl  13331  grpinvnz  13403  pwssub  13445  mhmmnd  13452  mulgfng  13460  mulgz  13486  mulgnndir  13487  mulgnn0dir  13488  mulgneg2  13492  mulgass  13495  mhmmulg  13499  issubgrpd2  13526  issubg4m  13529  grpissubg  13530  isnsg3  13543  ghmpreima  13602  ghmnsgpreima  13605  ghmf1  13609  conjnmz  13615  conjnmzb  13616  eqgabl  13666  gsumfzreidx  13673  gsumfzsubmcl  13674  gsumfzmptfidmadd  13675  gsumfzmhm  13679  rngpropd  13717  issrg  13727  ringpropd  13800  ringinvnz1ne0  13811  dvdsrvald  13855  dvdsrd  13856  dvdsrtr  13863  unitgrp  13878  rhmopp  13938  lmodfopne  14088  lmodprop2d  14110  lssvacl  14127  lsslss  14143  lss1d  14145  lsspropdg  14193  rnglidlmcl  14242  lidlacl  14246  isridl  14266  znidomb  14420  znunit  14421  znrrg  14422  psrval  14428  mplsubgfilemcl  14461  mplsubgfileminv  14462  mplsubgfi  14463  tgdom  14544  neipsm  14626  tgrest  14641  cnfval  14666  cnpfval  14667  cnpval  14670  iscnp4  14690  cnpnei  14691  cnptopco  14694  cncnpi  14700  cncnp  14702  cnptopresti  14710  cnptoprest2  14712  cndis  14713  lmtopcnp  14722  txbasval  14739  neitx  14740  txcnp  14743  txcnmpt  14745  txcn  14747  imasnopn  14771  psmetres2  14805  isxmet2d  14820  xblss2ps  14876  xblss2  14877  blbas  14905  neibl  14963  metss2lem  14969  metrest  14978  xmettx  14982  metcnp3  14983  metcnp  14984  metcnp2  14985  metcnpi  14987  metcnpi2  14988  mulc1cncf  15061  cncfco  15063  mulcncflem  15079  mulcncf  15080  dedekindeulemuub  15089  dedekindeulemloc  15091  dedekindeulemlu  15093  dedekindeu  15095  suplociccreex  15096  suplociccex  15097  dedekindicclemuub  15098  dedekindicclemloc  15100  dedekindicclemlu  15102  dedekindicclemicc  15104  dedekindicc  15105  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemloc  15113  ivthinc  15115  limcimolemlt  15136  limccnp2lem  15148  limccnp2cntop  15149  limccoap  15150  dvcj  15181  dvmptfsum  15197  dveflem  15198  plyf  15209  plyaddlem1  15219  plymullem1  15220  plycolemc  15230  plyco  15231  plycj  15233  dvply1  15237  dvply2g  15238  efltlemlt  15246  sin0pilem1  15253  sin0pilem2  15254  pilem3  15255  coseq0negpitopi  15308  abssinper  15318  cos02pilt1  15323  relogeftb  15337  logbgcd1irraplemexp  15440  logbgcd1irrap  15442  dvdsppwf1o  15461  mpodvdsmulf1o  15462  mersenne  15469  perfectlem2  15472  perfect  15473  lgsval  15481  lgsfvalg  15482  lgsfcl2  15483  lgsval2lem  15487  lgsmod  15503  lgsdilem  15504  lgsdir2lem4  15508  lgsdir2  15510  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem2  15559  2lgslem1a1  15563  2lgslem1a  15565  2sqlem5  15596  2sqlem6  15597  2sqlem7  15598  2sqlem9  15601  2sqlem10  15602  bj-findis  15915  2omap  15932  pwle2  15935  pwf1oexmid  15936  pw1nct  15940  nnsf  15942  peano4nninf  15943  nninfall  15946  nninfsellemeq  15951  nninfsellemeqinf  15953  nnnninfex  15959  nninfnfiinf  15960  qdencn  15966  refeq  15967  trilpolemeq1  15979  trilpolemlt1  15980  trirec0  15983  nconstwlpolemgt0  16003  nconstwlpolem  16004  neapmkvlem  16006