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  1263  vtoclgft  2851  reupick  3488  euotd  4341  frirrg  4441  ralxfrd  4553  nnsucpred  4709  foun  5593  f1oprg  5619  dffo4  5785  funopsn  5819  foeqcnvco  5920  fliftfun  5926  isotr  5946  riotass2  5989  ovmpodxf  6136  mpoxopoveq  6392  tfrlem1  6460  tfrlemibacc  6478  tfrlemibfn  6480  tfrlemi14d  6485  tfrexlem  6486  tfr1onlembacc  6494  tfr1onlembfn  6496  tfr1onlemres  6501  tfrcllembacc  6507  tfrcllembfn  6509  tfrcllemres  6514  frecabcl  6551  nnmordi  6670  eroprf  6783  f1imaen2g  6953  pw2f1odclem  7003  xpen  7014  mapen  7015  mapdom1g  7016  mapxpen  7017  xpmapenlem  7018  phplem4dom  7031  nndomo  7033  phpm  7035  fidifsnen  7040  dif1enen  7050  fisbth  7053  fimax2gtrilemstep  7071  fimax2gtri  7072  eqsndc  7076  en2eqpr  7080  unsnfidcex  7093  unsnfidcel  7094  ssfirab  7109  fidcenumlemrks  7131  sbthlemi8  7142  fiuni  7156  ordiso2  7213  updjud  7260  difinfsnlem  7277  ctssdclemn0  7288  ctssdccl  7289  ctssdc  7291  enumctlemm  7292  enumct  7293  nnnninfeq  7306  nninfisol  7311  enomnilem  7316  fodju0  7325  enmkvlem  7339  enwomnilem  7347  nninfwlpoimlemg  7353  pr1or2  7378  pr2cv1  7379  exmidfodomrlemim  7390  exmidontriimlem2  7415  exmidapne  7457  cc3  7465  dfplpq2  7552  nqpi  7576  nqnq0pi  7636  nq0nn  7640  elinp  7672  elnp1st2nd  7674  genprndl  7719  genprndu  7720  addnqprllem  7725  addnqprulem  7726  addnqprl  7727  addnqpru  7728  addlocpr  7734  nqprloc  7743  prmuloc  7764  mulnqprl  7766  mulnqpru  7767  mullocpr  7769  distrlem1prl  7780  distrlem1pru  7781  ltsopr  7794  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  aptiprleml  7837  aptiprlemu  7838  archpr  7841  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  archrecpr  7862  caucvgprlemnkj  7864  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprprlemnkltj  7887  caucvgprprlemnkeqj  7888  caucvgprprlemnjltk  7889  caucvgprprlemml  7892  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemdisj  7900  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  caucvgprprlemaddq  7906  suplocexprlemru  7917  suplocexprlemloc  7919  suplocexprlemex  7920  suplocexprlemub  7921  suplocexprlemlub  7922  mulgt0sr  7976  caucvgsrlemcau  7991  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axcaucvglemcau  8096  axcaucvglemres  8097  axpre-suploclemres  8099  axsuploc  8230  cnegexlem1  8332  cnegex  8335  apsym  8764  apcotr  8765  apadd1  8766  mulext1  8770  mulge0  8777  apti  8780  aprcl  8804  conjmulap  8887  lemulge11  9024  creui  9118  nndiv  9162  zaddcllemneg  9496  suprzclex  9556  eluzuzle  9742  infregelbex  9805  divfnzn  9828  qapne  9846  xrltso  10004  xnn0dcle  10010  xnn0letri  10011  xrre  10028  xrre3  10030  xaddf  10052  xaddval  10053  xpncan  10079  xleadd1a  10081  xltadd1  10084  xleaddadd  10095  ixxss12  10114  elioc2  10144  elico2  10145  elicc2  10146  fzm1  10308  fzneuz  10309  eluzgtdifelfzo  10415  elfzonelfzo  10448  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  suprzubdc  10468  nninfdcex  10469  zsupssdc  10470  qtri3or  10472  exbtwnzlemstep  10479  exbtwnzlemex  10481  exbtwnz  10482  modqid  10583  modqcyc2  10594  modqmuladd  10600  modqmuladdnn0  10602  modaddmodlo  10622  addmodlteq  10632  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgsuc  10648  frecuzrdgsuctlem  10657  nninfinf  10677  seq3clss  10705  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemab  10736  iseqf1olemmo  10739  iseqf1olemqf1o  10740  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1olemp  10749  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem1  10753  seqf1oglem2  10754  seqf1og  10755  seq3id3  10758  seqfeq4g  10765  ser3ge0  10770  exp3val  10775  expap0  10803  qsqeqor  10884  modqexp  10900  nn0ltexp2  10943  facndiv  10973  faclbnd  10975  bcval5  10997  hashunlem  11038  hashun  11039  hashprg  11043  fiprsshashgt1  11052  hashfacen  11071  zfz1isolemiso  11074  zfz1isolem1  11075  seq3coll  11077  ccatcl  11141  ccatlen  11143  ccatvalfn  11149  ccatsymb  11150  ccatrn  11157  swrdclg  11198  swrdspsleq  11215  pfxeq  11244  swrdswrd  11253  wrdind  11270  wrd2ind  11271  swrdccatin1  11273  swrdccatin2  11277  pfxccatin12  11281  pfxccat3  11282  swrdccat3b  11288  reuccatpfxs1  11295  ovshftex  11346  2shfti  11358  seq3shft  11365  cjap  11433  caucvgrelemcau  11507  cvg1nlemcau  11511  cvg1nlemres  11512  recvguniq  11522  resqrexlemdecn  11539  resqrexlemcalc3  11543  resqrexlemcvg  11546  resqrexlemoverl  11548  leabs  11601  absexpzap  11607  ltabs  11614  abslt  11615  absle  11616  maxleim  11732  maxabslemval  11735  fimaxre2  11754  minmax  11757  2zinfmin  11770  xrmaxiflemcl  11772  xrmaxifle  11773  xrmaxiflemab  11774  xrmaxiflemlub  11775  xrmaxiflemcom  11776  xrmaxltsup  11785  xrmaxadd  11788  xrminmax  11792  xrbdtri  11803  2clim  11828  climshftlemg  11829  climsqz  11862  climsqz2  11863  climrecvg1n  11875  climcvg1nlem  11876  serf0  11879  sumrbdclem  11904  fsum3cvg  11905  summodclem3  11907  summodclem2a  11908  summodclem2  11909  zsumdc  11911  fsum3  11914  isumss  11918  fisumss  11919  fsum3cvg3  11923  fsumcl2lem  11925  fsumadd  11933  fsumsplit  11934  sumsnf  11936  fsum2d  11962  fisum0diag2  11974  fsummulc2  11975  modfsummod  11985  fsumabs  11992  fsumrelem  11998  fsumiun  12004  geoisumr  12045  cvgratnnlemseq  12053  cvgratz  12059  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  prodrbdclem  12098  fproddccvg  12099  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  fprodseq  12110  fprodntrivap  12111  fprodssdc  12117  fprodmul  12118  prodsnf  12119  fprodsplitdc  12123  fprodsplit  12124  fprodunsn  12131  fprodcl2lem  12132  fprodap0  12148  fprod2d  12150  fprodrec  12156  fprodap0f  12163  efcj  12200  efaddlem  12201  tanaddaplem  12265  sinltxirr  12288  nndivides  12324  dvdsext  12382  divalglemeunn  12448  divalglemex  12449  divalglemeuneg  12450  bitsfzolem  12481  bitsmod  12483  bitsinv1  12489  dvdsbnd  12493  bezoutlemnewy  12533  bezoutlemstep  12534  bezoutlemmain  12535  bezoutlemzz  12539  bezoutlemaz  12540  bezoutlembz  12541  bezoutlemeu  12544  bezoutlemle  12545  bezoutlemsup  12546  dfgcd3  12547  dfgcd2  12551  bezoutr1  12570  nnmindc  12571  nninfctlemfo  12577  dvdslcm  12607  lcmgcdlem  12615  qredeq  12634  qredeu  12635  divgcdcoprm0  12639  divgcdcoprmex  12640  cncongr1  12641  isprm2lem  12654  prmind2  12658  exprmfct  12676  prmdvdsfz  12677  isprm5lem  12679  prmexpb  12689  rpexp1i  12692  sqrt2irr  12700  sqne2sq  12715  nonsq  12745  phiprmpw  12760  eulerthlemrprm  12767  eulerthlema  12768  hashgcdeq  12778  phisum  12779  modprmn0modprm0  12795  pclemub  12826  pclemdc  12827  pcmul  12840  pcqmul  12842  pcxqcl  12851  pcdvdstr  12866  pcprmpw2  12872  difsqpwdvds  12877  pcmpt  12882  oddprmdvds  12893  prmpwdvds  12894  pockthg  12896  infpnlem1  12898  1arith  12906  4sqlem2  12928  4sqlemafi  12934  4sqlemffi  12935  4sqleminfi  12936  4sqlem11  12940  4sqlem13m  12942  4sqlem14  12943  4sqlem17  12946  4sqlem18  12947  ennnfonelemg  12990  ennnfoneleminc  12998  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemfun  13004  ennnfonelemf1  13005  ennnfonelemrn  13006  ennnfonelemdm  13007  ennnfonelemnn0  13009  ennnfonelemim  13011  exmidunben  13013  ctinfomlemom  13014  ctinf  13017  ctiunctlemudc  13024  nninfdclemlt  13038  nninfdclemf1  13039  isstruct2r  13059  prdsval  13322  imasival  13355  gsumpropd2  13442  sgrppropd  13462  prdssgrpd  13464  mndpropd  13489  issubmnd  13491  prdsidlem  13496  prdsmndd  13497  pws0g  13500  mndissubm  13524  resmhm2b  13538  mhmeql  13541  gsumfzz  13544  gsumwsubmcl  13545  gsumwmhm  13547  gsumfzcl  13548  grpinvnz  13620  pwssub  13662  mhmmnd  13669  mulgfng  13677  mulgz  13703  mulgnndir  13704  mulgnn0dir  13705  mulgneg2  13709  mulgass  13712  mhmmulg  13716  issubgrpd2  13743  issubg4m  13746  grpissubg  13747  isnsg3  13760  ghmpreima  13819  ghmnsgpreima  13822  ghmf1  13826  conjnmz  13832  conjnmzb  13833  eqgabl  13883  gsumfzreidx  13890  gsumfzsubmcl  13891  gsumfzmptfidmadd  13892  gsumfzmhm  13896  rngpropd  13934  issrg  13944  ringpropd  14017  ringinvnz1ne0  14028  dvdsrvald  14073  dvdsrd  14074  dvdsrtr  14081  unitgrp  14096  rhmopp  14156  lmodfopne  14306  lmodprop2d  14328  lssvacl  14345  lsslss  14361  lss1d  14363  lsspropdg  14411  rnglidlmcl  14460  lidlacl  14464  isridl  14484  znidomb  14638  znunit  14639  znrrg  14640  psrval  14646  mplsubgfilemcl  14679  mplsubgfileminv  14680  mplsubgfi  14681  tgdom  14762  neipsm  14844  tgrest  14859  cnfval  14884  cnpfval  14885  cnpval  14888  iscnp4  14908  cnpnei  14909  cnptopco  14912  cncnpi  14918  cncnp  14920  cnptopresti  14928  cnptoprest2  14930  cndis  14931  lmtopcnp  14940  txbasval  14957  neitx  14958  txcnp  14961  txcnmpt  14963  txcn  14965  imasnopn  14989  psmetres2  15023  isxmet2d  15038  xblss2ps  15094  xblss2  15095  blbas  15123  neibl  15181  metss2lem  15187  metrest  15196  xmettx  15200  metcnp3  15201  metcnp  15202  metcnp2  15203  metcnpi  15205  metcnpi2  15206  mulc1cncf  15279  cncfco  15281  mulcncflem  15297  mulcncf  15298  dedekindeulemuub  15307  dedekindeulemloc  15309  dedekindeulemlu  15311  dedekindeu  15313  suplociccreex  15314  suplociccex  15315  dedekindicclemuub  15316  dedekindicclemloc  15318  dedekindicclemlu  15320  dedekindicclemicc  15322  dedekindicc  15323  ivthinclemlopn  15326  ivthinclemlr  15327  ivthinclemuopn  15328  ivthinclemur  15329  ivthinclemloc  15331  ivthinc  15333  limcimolemlt  15354  limccnp2lem  15366  limccnp2cntop  15367  limccoap  15368  dvcj  15399  dvmptfsum  15415  dveflem  15416  plyf  15427  plyaddlem1  15437  plymullem1  15438  plycolemc  15448  plyco  15449  plycj  15451  dvply1  15455  dvply2g  15456  efltlemlt  15464  sin0pilem1  15471  sin0pilem2  15472  pilem3  15473  coseq0negpitopi  15526  abssinper  15536  cos02pilt1  15541  relogeftb  15555  logbgcd1irraplemexp  15658  logbgcd1irrap  15660  dvdsppwf1o  15679  mpodvdsmulf1o  15680  mersenne  15687  perfectlem2  15690  perfect  15691  lgsval  15699  lgsfvalg  15700  lgsfcl2  15701  lgsval2lem  15705  lgsmod  15721  lgsdilem  15722  lgsdir2lem4  15726  lgsdir2  15728  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem1a  15753  gausslemma2dlem1f1o  15755  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem2  15777  2lgslem1a1  15781  2lgslem1a  15783  2sqlem5  15814  2sqlem6  15815  2sqlem7  15816  2sqlem9  15819  2sqlem10  15820  umgrnloopv  15930  uhgr2edg  16020  upgredginwlk  16102  clwwlkccatlem  16143  bj-findis  16425  2omap  16446  pwle2  16451  pwf1oexmid  16452  pw1nct  16456  nnsf  16459  peano4nninf  16460  nninfall  16463  nninfsellemeq  16468  nninfsellemeqinf  16470  nnnninfex  16476  nninfnfiinf  16477  qdencn  16483  refeq  16484  trilpolemeq1  16496  trilpolemlt1  16497  trirec0  16500  nconstwlpolemgt0  16520  nconstwlpolem  16521  neapmkvlem  16523