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  535  simpllr  536  ad5ant123  1266  vtoclgft  2867  reupick  3507  euotd  4373  frirrg  4473  ralxfrd  4585  nnsucpred  4741  foun  5635  f1oprg  5662  dffo4  5827  funopsn  5862  foeqcnvco  5965  fliftfun  5971  isotr  5991  riotass2  6034  ovmpodxf  6181  suppfnss  6459  suppcofn  6468  mpoxopoveq  6473  tfrlem1  6541  tfrlemibacc  6559  tfrlemibfn  6561  tfrlemi14d  6566  tfrexlem  6567  tfr1onlembacc  6575  tfr1onlembfn  6577  tfr1onlemres  6582  tfrcllembacc  6588  tfrcllembfn  6590  tfrcllemres  6595  frecabcl  6632  nnmordi  6751  eroprf  6864  mapsnd  6925  f1imaen2g  7035  pw2f1odclem  7089  xpen  7100  mapen  7101  mapdom1g  7102  mapxpen  7103  xpmapenlem  7104  phplem4dom  7118  nndomo  7120  phpm  7122  fidifsnen  7127  dif1enen  7139  fisbth  7142  fimax2gtrilemstep  7160  fimax2gtri  7161  eqsndc  7165  en2eqpr  7169  unsnfidcex  7182  unsnfidcel  7183  ssfirab  7199  fidcenumlemrks  7225  sbthlemi8  7236  fiuni  7267  2omap  7271  ordiso2  7328  updjud  7375  difinfsnlem  7392  ctssdclemn0  7403  ctssdccl  7404  ctssdc  7406  enumctlemm  7407  enumct  7408  nnnninfeq  7421  nninfisol  7426  enomnilem  7431  fodju0  7440  enmkvlem  7454  enwomnilem  7462  nninfwlpoimlemg  7468  pr1or2  7493  pr2cv1  7494  exmidfodomrlemim  7506  exmidontriimlem2  7531  exmidapne  7576  cc3  7584  dfplpq2  7671  nqpi  7695  nqnq0pi  7755  nq0nn  7759  elinp  7791  elnp1st2nd  7793  genprndl  7838  genprndu  7839  addnqprllem  7844  addnqprulem  7845  addnqprl  7846  addnqpru  7847  addlocpr  7853  nqprloc  7862  prmuloc  7883  mulnqprl  7885  mulnqpru  7886  mullocpr  7888  distrlem1prl  7899  distrlem1pru  7900  ltsopr  7913  ltexprlemopl  7918  ltexprlemopu  7920  ltexprlemloc  7924  ltexprlemrl  7927  ltexprlemru  7929  addcanprleml  7931  addcanprlemu  7932  recexprlemloc  7948  recexprlem1ssl  7950  recexprlem1ssu  7951  aptiprleml  7956  aptiprlemu  7957  archpr  7960  cauappcvgprlemm  7962  cauappcvgprlemopl  7963  cauappcvgprlemlol  7964  cauappcvgprlemladdfu  7971  cauappcvgprlemladdfl  7972  cauappcvgprlemladdru  7973  archrecpr  7981  caucvgprlemnkj  7983  caucvgprlemm  7985  caucvgprlemopl  7986  caucvgprlemlol  7987  caucvgprlemdisj  7991  caucvgprlemloc  7992  caucvgprlemladdfu  7994  caucvgprprlemnkltj  8006  caucvgprprlemnkeqj  8007  caucvgprprlemnjltk  8008  caucvgprprlemml  8011  caucvgprprlemopl  8014  caucvgprprlemlol  8015  caucvgprprlemdisj  8019  caucvgprprlemexbt  8023  caucvgprprlemexb  8024  caucvgprprlemaddq  8025  suplocexprlemru  8036  suplocexprlemloc  8038  suplocexprlemex  8039  suplocexprlemub  8040  suplocexprlemlub  8041  mulgt0sr  8095  caucvgsrlemcau  8110  caucvgsrlemoffcau  8115  caucvgsrlemoffres  8117  suplocsrlemb  8123  suplocsrlempr  8124  suplocsrlem  8125  axcaucvglemcau  8215  axcaucvglemres  8216  axpre-suploclemres  8218  axsuploc  8348  cnegexlem1  8450  cnegex  8453  apsym  8882  apcotr  8883  apadd1  8884  mulext1  8888  mulge0  8895  apti  8898  aprcl  8922  conjmulap  9005  lemulge11  9142  creui  9236  nndiv  9280  zaddcllemneg  9618  suprzclex  9679  eluzuzle  9865  infregelbex  9933  divfnzn  9956  qapne  9974  xrltso  10132  xnn0dcle  10138  xnn0letri  10139  xrre  10156  xrre3  10158  xaddf  10180  xaddval  10181  xpncan  10207  xleadd1a  10209  xltadd1  10212  xleaddadd  10223  ixxss12  10242  elioc2  10272  elico2  10273  elicc2  10274  fzm1  10438  fzneuz  10439  eluzgtdifelfzo  10546  elfzonelfzo  10579  exfzdc  10590  zsupcllemstep  10593  infssuzex  10597  suprzubdc  10600  nninfdcex  10601  zsupssdc  10602  qtri3or  10604  exbtwnzlemstep  10611  exbtwnzlemex  10613  exbtwnz  10614  modqid  10715  modqcyc2  10726  modqmuladd  10732  modqmuladdnn0  10734  modaddmodlo  10754  addmodlteq  10764  frecuzrdgrrn  10774  frec2uzrdg  10775  frecuzrdgsuc  10780  frecuzrdgsuctlem  10789  nninfinf  10809  seq3clss  10837  iseqf1olemqcl  10865  iseqf1olemnab  10867  iseqf1olemab  10868  iseqf1olemmo  10871  iseqf1olemqf1o  10872  iseqf1olemjpcl  10874  iseqf1olemqpcl  10875  seq3f1olemqsumk  10878  seq3f1olemqsum  10879  seq3f1olemp  10881  seq3f1oleml  10882  seq3f1o  10883  seqf1oglem1  10885  seqf1oglem2  10886  seqf1og  10887  seq3id3  10890  seqfeq4g  10897  ser3ge0  10902  exp3val  10907  expap0  10935  qsqeqor  11016  modqexp  11032  nn0ltexp2  11075  facndiv  11105  faclbnd  11107  bcval5  11129  hashunlem  11172  hashun  11173  hashprg  11177  fiprsshashgt1  11186  hashfacen  11212  zfz1isolemiso  11215  zfz1isolem1  11216  seq3coll  11218  hashtpglem  11222  ccatcl  11285  ccatlen  11287  ccatvalfn  11293  ccatsymb  11294  ccatrn  11301  ccat2s1fstg  11340  swrdclg  11346  swrdspsleq  11363  pfxeq  11392  swrdswrd  11401  wrdind  11418  wrd2ind  11419  swrdccatin1  11421  swrdccatin2  11425  pfxccatin12  11429  pfxccat3  11430  swrdccat3b  11436  reuccatpfxs1  11443  ovshftex  11508  2shfti  11520  seq3shft  11527  cjap  11595  caucvgrelemcau  11669  cvg1nlemcau  11673  cvg1nlemres  11674  recvguniq  11684  resqrexlemdecn  11701  resqrexlemcalc3  11705  resqrexlemcvg  11708  resqrexlemoverl  11710  leabs  11763  absexpzap  11769  ltabs  11776  abslt  11777  absle  11778  maxleim  11894  maxabslemval  11897  fimaxre2  11916  minmax  11919  2zinfmin  11932  xrmaxiflemcl  11934  xrmaxifle  11935  xrmaxiflemab  11936  xrmaxiflemlub  11937  xrmaxiflemcom  11938  xrmaxltsup  11947  xrmaxadd  11950  xrminmax  11954  xrbdtri  11965  2clim  11990  climshftlemg  11991  climsqz  12024  climsqz2  12025  climrecvg1n  12037  climcvg1nlem  12038  serf0  12041  sumrbdclem  12067  fsum3cvg  12068  summodclem3  12070  summodclem2a  12071  summodclem2  12072  zsumdc  12074  fsum3  12077  isumss  12081  fisumss  12082  fsum3cvg3  12086  fsumcl2lem  12088  fsumadd  12096  fsumsplit  12097  sumsnf  12099  fsum2d  12125  fisum0diag2  12137  fsummulc2  12138  modfsummod  12148  fsumabs  12155  fsumrelem  12161  fsumiun  12167  geoisumr  12208  cvgratnnlemseq  12216  cvgratz  12222  mertenslemi1  12225  mertenslem2  12226  mertensabs  12227  prodrbdclem  12261  fproddccvg  12262  prodmodclem3  12265  prodmodclem2a  12266  zproddc  12269  fprodseq  12273  fprodntrivap  12274  fprodssdc  12280  fprodmul  12281  prodsnf  12282  fprodsplitdc  12286  fprodsplit  12287  fprodunsn  12294  fprodcl2lem  12295  fprodap0  12311  fprod2d  12313  fprodrec  12319  fprodap0f  12326  efcj  12363  efaddlem  12364  tanaddaplem  12428  sinltxirr  12451  nndivides  12487  dvdsext  12545  divalglemeunn  12611  divalglemex  12612  divalglemeuneg  12613  bitsfzolem  12644  bitsmod  12646  bitsinv1  12652  dvdsbnd  12656  bezoutlemnewy  12696  bezoutlemstep  12697  bezoutlemmain  12698  bezoutlemzz  12702  bezoutlemaz  12703  bezoutlembz  12704  bezoutlemeu  12707  bezoutlemle  12708  bezoutlemsup  12709  dfgcd3  12710  dfgcd2  12714  bezoutr1  12733  nnmindc  12734  nninfctlemfo  12740  dvdslcm  12770  lcmgcdlem  12778  qredeq  12797  qredeu  12798  divgcdcoprm0  12802  divgcdcoprmex  12803  cncongr1  12804  isprm2lem  12817  prmind2  12821  exprmfct  12839  prmdvdsfz  12840  isprm5lem  12842  prmexpb  12852  rpexp1i  12855  sqrt2irr  12863  sqne2sq  12878  nonsq  12908  phiprmpw  12923  eulerthlemrprm  12930  eulerthlema  12931  hashgcdeq  12941  phisum  12942  modprmn0modprm0  12958  pclemub  12989  pclemdc  12990  pcmul  13003  pcqmul  13005  pcxqcl  13014  pcdvdstr  13029  pcprmpw2  13035  difsqpwdvds  13040  pcmpt  13045  oddprmdvds  13056  prmpwdvds  13057  pockthg  13059  infpnlem1  13061  1arith  13069  4sqlem2  13091  4sqlemafi  13097  4sqlemffi  13098  4sqleminfi  13099  4sqlem11  13103  4sqlem13m  13105  4sqlem14  13106  4sqlem17  13109  4sqlem18  13110  ennnfonelemg  13171  ennnfoneleminc  13179  ennnfonelemkh  13180  ennnfonelemhf1o  13181  ennnfonelemex  13182  ennnfonelemhom  13183  ennnfonelemfun  13185  ennnfonelemf1  13186  ennnfonelemrn  13187  ennnfonelemdm  13188  ennnfonelemnn0  13190  ennnfonelemim  13192  exmidunben  13194  ctinfomlemom  13195  ctinf  13198  ctiunctlemudc  13205  nninfdclemlt  13219  nninfdclemf1  13220  isstruct2r  13240  prdsval  13503  imasival  13536  gsumpropd2  13623  sgrppropd  13643  prdssgrpd  13645  mndpropd  13670  issubmnd  13672  prdsidlem  13677  prdsmndd  13678  pws0g  13681  mndissubm  13705  resmhm2b  13719  mhmeql  13722  gsumfzz  13725  gsumwsubmcl  13726  gsumwmhm  13728  gsumfzcl  13729  grpinvnz  13801  pwssub  13843  mhmmnd  13850  mulgfng  13858  mulgz  13884  mulgnndir  13885  mulgnn0dir  13886  mulgneg2  13890  mulgass  13893  mhmmulg  13897  issubgrpd2  13924  issubg4m  13927  grpissubg  13928  isnsg3  13941  ghmpreima  14000  ghmnsgpreima  14003  ghmf1  14007  conjnmz  14013  conjnmzb  14014  eqgabl  14064  gsumfzreidx  14071  gsumfzsubmcl  14072  gsumfzmptfidmadd  14073  gsumfzmhm  14077  rngpropd  14116  issrg  14126  ringpropd  14199  ringinvnz1ne0  14210  dvdsrvald  14255  dvdsrd  14256  dvdsrtr  14263  unitgrp  14278  rhmopp  14338  aprnzr  14450  lmodfopne  14491  lmodprop2d  14513  lssvacl  14530  lsslss  14546  lss1d  14548  lsspropdg  14596  rnglidlmcl  14645  lidlacl  14649  isridl  14669  znidomb  14823  znunit  14824  znrrg  14825  psrval  14831  mplsubgfilemcl  14871  mplsubgfileminv  14872  mplsubgfi  14873  tgdom  14954  neipsm  15036  tgrest  15051  cnfval  15076  cnpfval  15077  cnpval  15080  iscnp4  15100  cnpnei  15101  cnptopco  15104  cncnpi  15110  cncnp  15112  cnptopresti  15120  cnptoprest2  15122  cndis  15123  lmtopcnp  15132  txbasval  15149  neitx  15150  txcnp  15153  txcnmpt  15155  txcn  15157  imasnopn  15181  psmetres2  15215  isxmet2d  15230  xblss2ps  15286  xblss2  15287  blbas  15315  neibl  15373  metss2lem  15379  metrest  15388  xmettx  15392  metcnp3  15393  metcnp  15394  metcnp2  15395  metcnpi  15397  metcnpi2  15398  mulc1cncf  15471  cncfco  15473  mulcncflem  15489  mulcncf  15490  dedekindeulemuub  15499  dedekindeulemloc  15501  dedekindeulemlu  15503  dedekindeu  15505  suplociccreex  15506  suplociccex  15507  dedekindicclemuub  15508  dedekindicclemloc  15510  dedekindicclemlu  15512  dedekindicclemicc  15514  dedekindicc  15515  ivthinclemlopn  15518  ivthinclemlr  15519  ivthinclemuopn  15520  ivthinclemur  15521  ivthinclemloc  15523  ivthinc  15525  limcimolemlt  15546  limccnp2lem  15558  limccnp2cntop  15559  limccoap  15560  dvcj  15591  dvmptfsum  15607  dveflem  15608  plyf  15619  plyaddlem1  15629  plymullem1  15630  plycolemc  15640  plyco  15641  plycj  15643  dvply1  15647  dvply2g  15648  efltlemlt  15656  sin0pilem1  15663  sin0pilem2  15664  pilem3  15665  coseq0negpitopi  15718  abssinper  15728  cos02pilt1  15733  relogeftb  15747  logbgcd1irraplemexp  15850  logbgcd1irrap  15852  dvdsppwf1o  15874  mpodvdsmulf1o  15875  mersenne  15882  perfectlem2  15885  perfect  15886  lgsval  15894  lgsfvalg  15895  lgsfcl2  15896  lgsval2lem  15900  lgsmod  15916  lgsdilem  15917  lgsdir2lem4  15921  lgsdir2  15923  lgsdir  15925  lgsdilem2  15926  lgsdi  15927  lgsne0  15928  lgsdirnn0  15937  lgsdinn0  15938  gausslemma2dlem1a  15948  gausslemma2dlem1f1o  15950  lgsquadlem1  15967  lgsquadlem2  15968  lgsquad2lem2  15972  2lgslem1a1  15976  2lgslem1a  15978  2sqlem5  16009  2sqlem6  16010  2sqlem7  16011  2sqlem9  16014  2sqlem10  16015  umgrnloopv  16126  uhgr2edg  16218  upgredginwlk  16368  clwwlkccatlem  16412  eupth2lem3lem3fi  16482  eupth2lem3lem4fi  16485  eupth2lemsfi  16490  depindlem3  16520  bj-findis  16766  pwle2  16789  pwf1oexmid  16790  pw1nct  16794  nnsf  16800  peano4nninf  16801  nninfall  16804  nninfsellemeq  16809  nninfsellemeqinf  16811  nnnninfex  16817  nninfnfiinf  16818  qdencn  16824  refeq  16825  trilpolemeq1  16841  trilpolemlt1  16842  trirec0  16845  trimul0or  16862  nconstwlpolemgt0  16867  nconstwlpolem  16868  neapmkvlem  16870  gfsumval  16879  gfsumcl  16887