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  5591  f1oprg  5617  dffo4  5783  funopsn  5817  foeqcnvco  5914  fliftfun  5920  isotr  5940  riotass2  5983  ovmpodxf  6130  mpoxopoveq  6386  tfrlem1  6454  tfrlemibacc  6472  tfrlemibfn  6474  tfrlemi14d  6479  tfrexlem  6480  tfr1onlembacc  6488  tfr1onlembfn  6490  tfr1onlemres  6495  tfrcllembacc  6501  tfrcllembfn  6503  tfrcllemres  6508  frecabcl  6545  nnmordi  6662  eroprf  6775  f1imaen2g  6945  pw2f1odclem  6995  xpen  7006  mapen  7007  mapdom1g  7008  mapxpen  7009  xpmapenlem  7010  phplem4dom  7023  nndomo  7025  phpm  7027  fidifsnen  7032  dif1enen  7042  fisbth  7045  fimax2gtrilemstep  7062  fimax2gtri  7063  en2eqpr  7069  unsnfidcex  7082  unsnfidcel  7083  ssfirab  7098  fidcenumlemrks  7120  sbthlemi8  7131  fiuni  7145  ordiso2  7202  updjud  7249  difinfsnlem  7266  ctssdclemn0  7277  ctssdccl  7278  ctssdc  7280  enumctlemm  7281  enumct  7282  nnnninfeq  7295  nninfisol  7300  enomnilem  7305  fodju0  7314  enmkvlem  7328  enwomnilem  7336  nninfwlpoimlemg  7342  pr1or2  7367  pr2cv1  7368  exmidfodomrlemim  7379  exmidontriimlem2  7404  exmidapne  7446  cc3  7454  dfplpq2  7541  nqpi  7565  nqnq0pi  7625  nq0nn  7629  elinp  7661  elnp1st2nd  7663  genprndl  7708  genprndu  7709  addnqprllem  7714  addnqprulem  7715  addnqprl  7716  addnqpru  7717  addlocpr  7723  nqprloc  7732  prmuloc  7753  mulnqprl  7755  mulnqpru  7756  mullocpr  7758  distrlem1prl  7769  distrlem1pru  7770  ltsopr  7783  ltexprlemopl  7788  ltexprlemopu  7790  ltexprlemloc  7794  ltexprlemrl  7797  ltexprlemru  7799  addcanprleml  7801  addcanprlemu  7802  recexprlemloc  7818  recexprlem1ssl  7820  recexprlem1ssu  7821  aptiprleml  7826  aptiprlemu  7827  archpr  7830  cauappcvgprlemm  7832  cauappcvgprlemopl  7833  cauappcvgprlemlol  7834  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  cauappcvgprlemladdru  7843  archrecpr  7851  caucvgprlemnkj  7853  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemlol  7857  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprlemladdfu  7864  caucvgprprlemnkltj  7876  caucvgprprlemnkeqj  7877  caucvgprprlemnjltk  7878  caucvgprprlemml  7881  caucvgprprlemopl  7884  caucvgprprlemlol  7885  caucvgprprlemdisj  7889  caucvgprprlemexbt  7893  caucvgprprlemexb  7894  caucvgprprlemaddq  7895  suplocexprlemru  7906  suplocexprlemloc  7908  suplocexprlemex  7909  suplocexprlemub  7910  suplocexprlemlub  7911  mulgt0sr  7965  caucvgsrlemcau  7980  caucvgsrlemoffcau  7985  caucvgsrlemoffres  7987  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  axcaucvglemcau  8085  axcaucvglemres  8086  axpre-suploclemres  8088  axsuploc  8219  cnegexlem1  8321  cnegex  8324  apsym  8753  apcotr  8754  apadd1  8755  mulext1  8759  mulge0  8766  apti  8769  aprcl  8793  conjmulap  8876  lemulge11  9013  creui  9107  nndiv  9151  zaddcllemneg  9485  suprzclex  9545  eluzuzle  9730  infregelbex  9793  divfnzn  9816  qapne  9834  xrltso  9992  xnn0dcle  9998  xnn0letri  9999  xrre  10016  xrre3  10018  xaddf  10040  xaddval  10041  xpncan  10067  xleadd1a  10069  xltadd1  10072  xleaddadd  10083  ixxss12  10102  elioc2  10132  elico2  10133  elicc2  10134  fzm1  10296  fzneuz  10297  eluzgtdifelfzo  10403  elfzonelfzo  10436  exfzdc  10446  zsupcllemstep  10449  infssuzex  10453  suprzubdc  10456  nninfdcex  10457  zsupssdc  10458  qtri3or  10460  exbtwnzlemstep  10467  exbtwnzlemex  10469  exbtwnz  10470  modqid  10571  modqcyc2  10582  modqmuladd  10588  modqmuladdnn0  10590  modaddmodlo  10610  addmodlteq  10620  frecuzrdgrrn  10630  frec2uzrdg  10631  frecuzrdgsuc  10636  frecuzrdgsuctlem  10645  nninfinf  10665  seq3clss  10693  iseqf1olemqcl  10721  iseqf1olemnab  10723  iseqf1olemab  10724  iseqf1olemmo  10727  iseqf1olemqf1o  10728  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  seq3f1olemqsumk  10734  seq3f1olemqsum  10735  seq3f1olemp  10737  seq3f1oleml  10738  seq3f1o  10739  seqf1oglem1  10741  seqf1oglem2  10742  seqf1og  10743  seq3id3  10746  seqfeq4g  10753  ser3ge0  10758  exp3val  10763  expap0  10791  qsqeqor  10872  modqexp  10888  nn0ltexp2  10931  facndiv  10961  faclbnd  10963  bcval5  10985  hashunlem  11026  hashun  11027  hashprg  11030  fiprsshashgt1  11039  hashfacen  11058  zfz1isolemiso  11061  zfz1isolem1  11062  seq3coll  11064  ccatcl  11128  ccatlen  11130  ccatvalfn  11136  ccatsymb  11137  ccatrn  11144  swrdclg  11182  swrdspsleq  11199  pfxeq  11228  swrdswrd  11237  wrdind  11254  wrd2ind  11255  swrdccatin1  11257  swrdccatin2  11261  pfxccatin12  11265  pfxccat3  11266  swrdccat3b  11272  reuccatpfxs1  11279  ovshftex  11330  2shfti  11342  seq3shft  11349  cjap  11417  caucvgrelemcau  11491  cvg1nlemcau  11495  cvg1nlemres  11496  recvguniq  11506  resqrexlemdecn  11523  resqrexlemcalc3  11527  resqrexlemcvg  11530  resqrexlemoverl  11532  leabs  11585  absexpzap  11591  ltabs  11598  abslt  11599  absle  11600  maxleim  11716  maxabslemval  11719  fimaxre2  11738  minmax  11741  2zinfmin  11754  xrmaxiflemcl  11756  xrmaxifle  11757  xrmaxiflemab  11758  xrmaxiflemlub  11759  xrmaxiflemcom  11760  xrmaxltsup  11769  xrmaxadd  11772  xrminmax  11776  xrbdtri  11787  2clim  11812  climshftlemg  11813  climsqz  11846  climsqz2  11847  climrecvg1n  11859  climcvg1nlem  11860  serf0  11863  sumrbdclem  11888  fsum3cvg  11889  summodclem3  11891  summodclem2a  11892  summodclem2  11893  zsumdc  11895  fsum3  11898  isumss  11902  fisumss  11903  fsum3cvg3  11907  fsumcl2lem  11909  fsumadd  11917  fsumsplit  11918  sumsnf  11920  fsum2d  11946  fisum0diag2  11958  fsummulc2  11959  modfsummod  11969  fsumabs  11976  fsumrelem  11982  fsumiun  11988  geoisumr  12029  cvgratnnlemseq  12037  cvgratz  12043  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  prodrbdclem  12082  fproddccvg  12083  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  fprodntrivap  12095  fprodssdc  12101  fprodmul  12102  prodsnf  12103  fprodsplitdc  12107  fprodsplit  12108  fprodunsn  12115  fprodcl2lem  12116  fprodap0  12132  fprod2d  12134  fprodrec  12140  fprodap0f  12147  efcj  12184  efaddlem  12185  tanaddaplem  12249  sinltxirr  12272  nndivides  12308  dvdsext  12366  divalglemeunn  12432  divalglemex  12433  divalglemeuneg  12434  bitsfzolem  12465  bitsmod  12467  bitsinv1  12473  dvdsbnd  12477  bezoutlemnewy  12517  bezoutlemstep  12518  bezoutlemmain  12519  bezoutlemzz  12523  bezoutlemaz  12524  bezoutlembz  12525  bezoutlemeu  12528  bezoutlemle  12529  bezoutlemsup  12530  dfgcd3  12531  dfgcd2  12535  bezoutr1  12554  nnmindc  12555  nninfctlemfo  12561  dvdslcm  12591  lcmgcdlem  12599  qredeq  12618  qredeu  12619  divgcdcoprm0  12623  divgcdcoprmex  12624  cncongr1  12625  isprm2lem  12638  prmind2  12642  exprmfct  12660  prmdvdsfz  12661  isprm5lem  12663  prmexpb  12673  rpexp1i  12676  sqrt2irr  12684  sqne2sq  12699  nonsq  12729  phiprmpw  12744  eulerthlemrprm  12751  eulerthlema  12752  hashgcdeq  12762  phisum  12763  modprmn0modprm0  12779  pclemub  12810  pclemdc  12811  pcmul  12824  pcqmul  12826  pcxqcl  12835  pcdvdstr  12850  pcprmpw2  12856  difsqpwdvds  12861  pcmpt  12866  oddprmdvds  12877  prmpwdvds  12878  pockthg  12880  infpnlem1  12882  1arith  12890  4sqlem2  12912  4sqlemafi  12918  4sqlemffi  12919  4sqleminfi  12920  4sqlem11  12924  4sqlem13m  12926  4sqlem14  12927  4sqlem17  12930  4sqlem18  12931  ennnfonelemg  12974  ennnfoneleminc  12982  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemfun  12988  ennnfonelemf1  12989  ennnfonelemrn  12990  ennnfonelemdm  12991  ennnfonelemnn0  12993  ennnfonelemim  12995  exmidunben  12997  ctinfomlemom  12998  ctinf  13001  ctiunctlemudc  13008  nninfdclemlt  13022  nninfdclemf1  13023  isstruct2r  13043  prdsval  13306  imasival  13339  gsumpropd2  13426  sgrppropd  13446  prdssgrpd  13448  mndpropd  13473  issubmnd  13475  prdsidlem  13480  prdsmndd  13481  pws0g  13484  mndissubm  13508  resmhm2b  13522  mhmeql  13525  gsumfzz  13528  gsumwsubmcl  13529  gsumwmhm  13531  gsumfzcl  13532  grpinvnz  13604  pwssub  13646  mhmmnd  13653  mulgfng  13661  mulgz  13687  mulgnndir  13688  mulgnn0dir  13689  mulgneg2  13693  mulgass  13696  mhmmulg  13700  issubgrpd2  13727  issubg4m  13730  grpissubg  13731  isnsg3  13744  ghmpreima  13803  ghmnsgpreima  13806  ghmf1  13810  conjnmz  13816  conjnmzb  13817  eqgabl  13867  gsumfzreidx  13874  gsumfzsubmcl  13875  gsumfzmptfidmadd  13876  gsumfzmhm  13880  rngpropd  13918  issrg  13928  ringpropd  14001  ringinvnz1ne0  14012  dvdsrvald  14057  dvdsrd  14058  dvdsrtr  14065  unitgrp  14080  rhmopp  14140  lmodfopne  14290  lmodprop2d  14312  lssvacl  14329  lsslss  14345  lss1d  14347  lsspropdg  14395  rnglidlmcl  14444  lidlacl  14448  isridl  14468  znidomb  14622  znunit  14623  znrrg  14624  psrval  14630  mplsubgfilemcl  14663  mplsubgfileminv  14664  mplsubgfi  14665  tgdom  14746  neipsm  14828  tgrest  14843  cnfval  14868  cnpfval  14869  cnpval  14872  iscnp4  14892  cnpnei  14893  cnptopco  14896  cncnpi  14902  cncnp  14904  cnptopresti  14912  cnptoprest2  14914  cndis  14915  lmtopcnp  14924  txbasval  14941  neitx  14942  txcnp  14945  txcnmpt  14947  txcn  14949  imasnopn  14973  psmetres2  15007  isxmet2d  15022  xblss2ps  15078  xblss2  15079  blbas  15107  neibl  15165  metss2lem  15171  metrest  15180  xmettx  15184  metcnp3  15185  metcnp  15186  metcnp2  15187  metcnpi  15189  metcnpi2  15190  mulc1cncf  15263  cncfco  15265  mulcncflem  15281  mulcncf  15282  dedekindeulemuub  15291  dedekindeulemloc  15293  dedekindeulemlu  15295  dedekindeu  15297  suplociccreex  15298  suplociccex  15299  dedekindicclemuub  15300  dedekindicclemloc  15302  dedekindicclemlu  15304  dedekindicclemicc  15306  dedekindicc  15307  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemloc  15315  ivthinc  15317  limcimolemlt  15338  limccnp2lem  15350  limccnp2cntop  15351  limccoap  15352  dvcj  15383  dvmptfsum  15399  dveflem  15400  plyf  15411  plyaddlem1  15421  plymullem1  15422  plycolemc  15432  plyco  15433  plycj  15435  dvply1  15439  dvply2g  15440  efltlemlt  15448  sin0pilem1  15455  sin0pilem2  15456  pilem3  15457  coseq0negpitopi  15510  abssinper  15520  cos02pilt1  15525  relogeftb  15539  logbgcd1irraplemexp  15642  logbgcd1irrap  15644  dvdsppwf1o  15663  mpodvdsmulf1o  15664  mersenne  15671  perfectlem2  15674  perfect  15675  lgsval  15683  lgsfvalg  15684  lgsfcl2  15685  lgsval2lem  15689  lgsmod  15705  lgsdilem  15706  lgsdir2lem4  15710  lgsdir2  15712  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem1a  15737  gausslemma2dlem1f1o  15739  lgsquadlem1  15756  lgsquadlem2  15757  lgsquad2lem2  15761  2lgslem1a1  15765  2lgslem1a  15767  2sqlem5  15798  2sqlem6  15799  2sqlem7  15800  2sqlem9  15803  2sqlem10  15804  umgrnloopv  15914  uhgr2edg  16004  upgredginwlk  16067  bj-findis  16342  2omap  16359  pwle2  16364  pwf1oexmid  16365  pw1nct  16369  nnsf  16371  peano4nninf  16372  nninfall  16375  nninfsellemeq  16380  nninfsellemeqinf  16382  nnnninfex  16388  nninfnfiinf  16389  qdencn  16395  refeq  16396  trilpolemeq1  16408  trilpolemlt1  16409  trirec0  16412  nconstwlpolemgt0  16432  nconstwlpolem  16433  neapmkvlem  16435