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  1241  vtoclgft  2811  reupick  3444  euotd  4284  frirrg  4382  ralxfrd  4494  nnsucpred  4650  foun  5520  f1oprg  5545  dffo4  5707  foeqcnvco  5834  fliftfun  5840  isotr  5860  riotass2  5901  ovmpodxf  6045  mpoxopoveq  6295  tfrlem1  6363  tfrlemibacc  6381  tfrlemibfn  6383  tfrlemi14d  6388  tfrexlem  6389  tfr1onlembacc  6397  tfr1onlembfn  6399  tfr1onlemres  6404  tfrcllembacc  6410  tfrcllembfn  6412  tfrcllemres  6417  frecabcl  6454  nnmordi  6571  eroprf  6684  f1imaen2g  6849  pw2f1odclem  6892  xpen  6903  mapen  6904  mapdom1g  6905  mapxpen  6906  xpmapenlem  6907  phplem4dom  6920  nndomo  6922  phpm  6923  fidifsnen  6928  dif1enen  6938  fisbth  6941  fimax2gtrilemstep  6958  fimax2gtri  6959  en2eqpr  6965  unsnfidcex  6978  unsnfidcel  6979  ssfirab  6992  fidcenumlemrks  7014  sbthlemi8  7025  fiuni  7039  ordiso2  7096  updjud  7143  difinfsnlem  7160  ctssdclemn0  7171  ctssdccl  7172  ctssdc  7174  enumctlemm  7175  enumct  7176  nnnninfeq  7189  nninfisol  7194  enomnilem  7199  fodju0  7208  enmkvlem  7222  enwomnilem  7230  nninfwlpoimlemg  7236  exmidfodomrlemim  7263  exmidontriimlem2  7284  exmidapne  7322  cc3  7330  dfplpq2  7416  nqpi  7440  nqnq0pi  7500  nq0nn  7504  elinp  7536  elnp1st2nd  7538  genprndl  7583  genprndu  7584  addnqprllem  7589  addnqprulem  7590  addnqprl  7591  addnqpru  7592  addlocpr  7598  nqprloc  7607  prmuloc  7628  mulnqprl  7630  mulnqpru  7631  mullocpr  7633  distrlem1prl  7644  distrlem1pru  7645  ltsopr  7658  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemloc  7669  ltexprlemrl  7672  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  recexprlemloc  7693  recexprlem1ssl  7695  recexprlem1ssu  7696  aptiprleml  7701  aptiprlemu  7702  archpr  7705  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  archrecpr  7726  caucvgprlemnkj  7728  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemladdfu  7739  caucvgprprlemnkltj  7751  caucvgprprlemnkeqj  7752  caucvgprprlemnjltk  7753  caucvgprprlemml  7756  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemdisj  7764  caucvgprprlemexbt  7768  caucvgprprlemexb  7769  caucvgprprlemaddq  7770  suplocexprlemru  7781  suplocexprlemloc  7783  suplocexprlemex  7784  suplocexprlemub  7785  suplocexprlemlub  7786  mulgt0sr  7840  caucvgsrlemcau  7855  caucvgsrlemoffcau  7860  caucvgsrlemoffres  7862  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  axcaucvglemcau  7960  axcaucvglemres  7961  axpre-suploclemres  7963  axsuploc  8094  cnegexlem1  8196  cnegex  8199  apsym  8627  apcotr  8628  apadd1  8629  mulext1  8633  mulge0  8640  apti  8643  aprcl  8667  conjmulap  8750  lemulge11  8887  creui  8981  nndiv  9025  zaddcllemneg  9359  suprzclex  9418  eluzuzle  9603  infregelbex  9666  divfnzn  9689  qapne  9707  xrltso  9865  xnn0dcle  9871  xnn0letri  9872  xrre  9889  xrre3  9891  xaddf  9913  xaddval  9914  xpncan  9940  xleadd1a  9942  xltadd1  9945  xleaddadd  9956  ixxss12  9975  elioc2  10005  elico2  10006  elicc2  10007  fzm1  10169  fzneuz  10170  eluzgtdifelfzo  10267  elfzonelfzo  10300  exfzdc  10310  qtri3or  10313  exbtwnzlemstep  10319  exbtwnzlemex  10321  exbtwnz  10322  modqid  10423  modqcyc2  10434  modqmuladd  10440  modqmuladdnn0  10442  modaddmodlo  10462  addmodlteq  10472  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgsuc  10488  frecuzrdgsuctlem  10497  nninfinf  10517  seq3clss  10545  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemab  10576  iseqf1olemmo  10579  iseqf1olemqf1o  10580  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seq3f1olemp  10589  seq3f1oleml  10590  seq3f1o  10591  seqf1oglem1  10593  seqf1oglem2  10594  seqf1og  10595  seq3id3  10598  seqfeq4g  10605  ser3ge0  10610  exp3val  10615  expap0  10643  qsqeqor  10724  modqexp  10740  nn0ltexp2  10783  facndiv  10813  faclbnd  10815  bcval5  10837  hashunlem  10878  hashun  10879  hashprg  10882  fiprsshashgt1  10891  hashfacen  10910  zfz1isolemiso  10913  zfz1isolem1  10914  seq3coll  10916  ovshftex  10966  2shfti  10978  seq3shft  10985  cjap  11053  caucvgrelemcau  11127  cvg1nlemcau  11131  cvg1nlemres  11132  recvguniq  11142  resqrexlemdecn  11159  resqrexlemcalc3  11163  resqrexlemcvg  11166  resqrexlemoverl  11168  leabs  11221  absexpzap  11227  ltabs  11234  abslt  11235  absle  11236  maxleim  11352  maxabslemval  11355  fimaxre2  11373  minmax  11376  2zinfmin  11389  xrmaxiflemcl  11391  xrmaxifle  11392  xrmaxiflemab  11393  xrmaxiflemlub  11394  xrmaxiflemcom  11395  xrmaxltsup  11404  xrmaxadd  11407  xrminmax  11411  xrbdtri  11422  2clim  11447  climshftlemg  11448  climsqz  11481  climsqz2  11482  climrecvg1n  11494  climcvg1nlem  11495  serf0  11498  sumrbdclem  11523  fsum3cvg  11524  summodclem3  11526  summodclem2a  11527  summodclem2  11528  zsumdc  11530  fsum3  11533  isumss  11537  fisumss  11538  fsum3cvg3  11542  fsumcl2lem  11544  fsumadd  11552  fsumsplit  11553  sumsnf  11555  fsum2d  11581  fisum0diag2  11593  fsummulc2  11594  modfsummod  11604  fsumabs  11611  fsumrelem  11617  fsumiun  11623  geoisumr  11664  cvgratnnlemseq  11672  cvgratz  11678  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodrbdclem  11717  fproddccvg  11718  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  fprodntrivap  11730  fprodssdc  11736  fprodmul  11737  prodsnf  11738  fprodsplitdc  11742  fprodsplit  11743  fprodunsn  11750  fprodcl2lem  11751  fprodap0  11767  fprod2d  11769  fprodrec  11775  fprodap0f  11782  efcj  11819  efaddlem  11820  tanaddaplem  11884  sinltxirr  11907  nndivides  11943  dvdsext  12000  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  zsupcllemstep  12085  infssuzex  12089  suprzubdc  12092  nninfdcex  12093  zsupssdc  12094  dvdsbnd  12096  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlemzz  12142  bezoutlemaz  12143  bezoutlembz  12144  bezoutlemeu  12147  bezoutlemle  12148  bezoutlemsup  12149  dfgcd3  12150  dfgcd2  12154  bezoutr1  12173  nnmindc  12174  nninfctlemfo  12180  dvdslcm  12210  lcmgcdlem  12218  qredeq  12237  qredeu  12238  divgcdcoprm0  12242  divgcdcoprmex  12243  cncongr1  12244  isprm2lem  12257  prmind2  12261  exprmfct  12279  prmdvdsfz  12280  isprm5lem  12282  prmexpb  12292  rpexp1i  12295  sqrt2irr  12303  sqne2sq  12318  nonsq  12348  phiprmpw  12363  eulerthlemrprm  12370  eulerthlema  12371  hashgcdeq  12380  phisum  12381  modprmn0modprm0  12397  pclemub  12428  pclemdc  12429  pcmul  12442  pcqmul  12444  pcxqcl  12453  pcdvdstr  12468  pcprmpw2  12474  difsqpwdvds  12479  pcmpt  12484  oddprmdvds  12495  prmpwdvds  12496  pockthg  12498  infpnlem1  12500  1arith  12508  4sqlem2  12530  4sqlemafi  12536  4sqlemffi  12537  4sqleminfi  12538  4sqlem11  12542  4sqlem13m  12544  4sqlem14  12545  4sqlem17  12548  4sqlem18  12549  ennnfonelemg  12563  ennnfoneleminc  12571  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemfun  12577  ennnfonelemf1  12578  ennnfonelemrn  12579  ennnfonelemdm  12580  ennnfonelemnn0  12582  ennnfonelemim  12584  exmidunben  12586  ctinfomlemom  12587  ctinf  12590  ctiunctlemudc  12597  nninfdclemlt  12611  nninfdclemf1  12612  isstruct2r  12632  imasival  12892  gsumpropd2  12979  sgrppropd  12999  mndpropd  13024  issubmnd  13026  mndissubm  13050  resmhm2b  13064  mhmeql  13067  gsumfzz  13070  gsumwsubmcl  13071  gsumwmhm  13073  gsumfzcl  13074  grpinvnz  13146  mhmmnd  13189  mulgfng  13197  mulgz  13223  mulgnndir  13224  mulgnn0dir  13225  mulgneg2  13229  mulgass  13232  mhmmulg  13236  issubgrpd2  13263  issubg4m  13266  grpissubg  13267  isnsg3  13280  ghmpreima  13339  ghmnsgpreima  13342  ghmf1  13346  conjnmz  13352  conjnmzb  13353  eqgabl  13403  gsumfzreidx  13410  gsumfzsubmcl  13411  gsumfzmptfidmadd  13412  gsumfzmhm  13416  rngpropd  13454  issrg  13464  ringpropd  13537  ringinvnz1ne0  13548  dvdsrvald  13592  dvdsrd  13593  dvdsrtr  13600  unitgrp  13615  rhmopp  13675  lmodfopne  13825  lmodprop2d  13847  lssvacl  13864  lsslss  13880  lss1d  13882  lsspropdg  13930  rnglidlmcl  13979  lidlacl  13983  isridl  14003  znidomb  14157  znunit  14158  znrrg  14159  psrval  14163  tgdom  14251  neipsm  14333  tgrest  14348  cnfval  14373  cnpfval  14374  cnpval  14377  iscnp4  14397  cnpnei  14398  cnptopco  14401  cncnpi  14407  cncnp  14409  cnptopresti  14417  cnptoprest2  14419  cndis  14420  lmtopcnp  14429  txbasval  14446  neitx  14447  txcnp  14450  txcnmpt  14452  txcn  14454  imasnopn  14478  psmetres2  14512  isxmet2d  14527  xblss2ps  14583  xblss2  14584  blbas  14612  neibl  14670  metss2lem  14676  metrest  14685  xmettx  14689  metcnp3  14690  metcnp  14691  metcnp2  14692  metcnpi  14694  metcnpi2  14695  mulc1cncf  14768  cncfco  14770  mulcncflem  14786  mulcncf  14787  dedekindeulemuub  14796  dedekindeulemloc  14798  dedekindeulemlu  14800  dedekindeu  14802  suplociccreex  14803  suplociccex  14804  dedekindicclemuub  14805  dedekindicclemloc  14807  dedekindicclemlu  14809  dedekindicclemicc  14811  dedekindicc  14812  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemloc  14820  ivthinc  14822  limcimolemlt  14843  limccnp2lem  14855  limccnp2cntop  14856  limccoap  14857  dvcj  14888  dvmptfsum  14904  dveflem  14905  plyf  14916  plyaddlem1  14926  plymullem1  14927  plycolemc  14936  plyco  14937  plycj  14939  dvply1  14943  efltlemlt  14950  sin0pilem1  14957  sin0pilem2  14958  pilem3  14959  coseq0negpitopi  15012  abssinper  15022  cos02pilt1  15027  relogeftb  15041  logbgcd1irraplemexp  15141  logbgcd1irrap  15143  lgsval  15161  lgsfvalg  15162  lgsfcl2  15163  lgsval2lem  15167  lgsmod  15183  lgsdilem  15184  lgsdir2lem4  15188  lgsdir2  15190  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem2  15239  2lgslem1a1  15243  2lgslem1a  15245  2sqlem5  15276  2sqlem6  15277  2sqlem7  15278  2sqlem9  15281  2sqlem10  15282  bj-findis  15541  pwle2  15559  pwf1oexmid  15560  pw1nct  15563  nnsf  15565  peano4nninf  15566  nninfall  15569  nninfsellemeq  15574  nninfsellemeqinf  15576  qdencn  15587  refeq  15588  trilpolemeq1  15600  trilpolemlt1  15601  trirec0  15604  nconstwlpolemgt0  15624  nconstwlpolem  15625  neapmkvlem  15627