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  1265  vtoclgft  2854  reupick  3491  euotd  4347  frirrg  4447  ralxfrd  4559  nnsucpred  4715  foun  5602  f1oprg  5629  dffo4  5795  funopsn  5830  foeqcnvco  5931  fliftfun  5937  isotr  5957  riotass2  6000  ovmpodxf  6147  mpoxopoveq  6406  tfrlem1  6474  tfrlemibacc  6492  tfrlemibfn  6494  tfrlemi14d  6499  tfrexlem  6500  tfr1onlembacc  6508  tfr1onlembfn  6510  tfr1onlemres  6515  tfrcllembacc  6521  tfrcllembfn  6523  tfrcllemres  6528  frecabcl  6565  nnmordi  6684  eroprf  6797  f1imaen2g  6967  pw2f1odclem  7020  xpen  7031  mapen  7032  mapdom1g  7033  mapxpen  7034  xpmapenlem  7035  phplem4dom  7048  nndomo  7050  phpm  7052  fidifsnen  7057  dif1enen  7069  fisbth  7072  fimax2gtrilemstep  7090  fimax2gtri  7091  eqsndc  7095  en2eqpr  7099  unsnfidcex  7112  unsnfidcel  7113  ssfirab  7129  fidcenumlemrks  7152  sbthlemi8  7163  fiuni  7177  ordiso2  7234  updjud  7281  difinfsnlem  7298  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  enumct  7314  nnnninfeq  7327  nninfisol  7332  enomnilem  7337  fodju0  7346  enmkvlem  7360  enwomnilem  7368  nninfwlpoimlemg  7374  pr1or2  7399  pr2cv1  7400  exmidfodomrlemim  7412  exmidontriimlem2  7437  exmidapne  7479  cc3  7487  dfplpq2  7574  nqpi  7598  nqnq0pi  7658  nq0nn  7662  elinp  7694  elnp1st2nd  7696  genprndl  7741  genprndu  7742  addnqprllem  7747  addnqprulem  7748  addnqprl  7749  addnqpru  7750  addlocpr  7756  nqprloc  7765  prmuloc  7786  mulnqprl  7788  mulnqpru  7789  mullocpr  7791  distrlem1prl  7802  distrlem1pru  7803  ltsopr  7816  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  aptiprleml  7859  aptiprlemu  7860  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  archrecpr  7884  caucvgprlemnkj  7886  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnjltk  7911  caucvgprprlemml  7914  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemdisj  7922  caucvgprprlemexbt  7926  caucvgprprlemexb  7927  caucvgprprlemaddq  7928  suplocexprlemru  7939  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  suplocexprlemlub  7944  mulgt0sr  7998  caucvgsrlemcau  8013  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  axsuploc  8252  cnegexlem1  8354  cnegex  8357  apsym  8786  apcotr  8787  apadd1  8788  mulext1  8792  mulge0  8799  apti  8802  aprcl  8826  conjmulap  8909  lemulge11  9046  creui  9140  nndiv  9184  zaddcllemneg  9518  suprzclex  9578  eluzuzle  9764  infregelbex  9832  divfnzn  9855  qapne  9873  xrltso  10031  xnn0dcle  10037  xnn0letri  10038  xrre  10055  xrre3  10057  xaddf  10079  xaddval  10080  xpncan  10106  xleadd1a  10108  xltadd1  10111  xleaddadd  10122  ixxss12  10141  elioc2  10171  elico2  10172  elicc2  10173  fzm1  10335  fzneuz  10336  eluzgtdifelfzo  10443  elfzonelfzo  10476  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  nninfdcex  10498  zsupssdc  10499  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemex  10510  exbtwnz  10511  modqid  10612  modqcyc2  10623  modqmuladd  10629  modqmuladdnn0  10631  modaddmodlo  10651  addmodlteq  10661  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgsuc  10677  frecuzrdgsuctlem  10686  nninfinf  10706  seq3clss  10734  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemmo  10768  iseqf1olemqf1o  10769  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemp  10778  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  seq3id3  10787  seqfeq4g  10794  ser3ge0  10799  exp3val  10804  expap0  10832  qsqeqor  10913  modqexp  10929  nn0ltexp2  10972  facndiv  11002  faclbnd  11004  bcval5  11026  hashunlem  11068  hashun  11069  hashprg  11073  fiprsshashgt1  11082  hashfacen  11101  zfz1isolemiso  11104  zfz1isolem1  11105  seq3coll  11107  hashtpglem  11111  ccatcl  11174  ccatlen  11176  ccatvalfn  11182  ccatsymb  11183  ccatrn  11190  ccat2s1fstg  11229  swrdclg  11235  swrdspsleq  11252  pfxeq  11281  swrdswrd  11290  wrdind  11307  wrd2ind  11308  swrdccatin1  11310  swrdccatin2  11314  pfxccatin12  11318  pfxccat3  11319  swrdccat3b  11325  reuccatpfxs1  11332  ovshftex  11397  2shfti  11409  seq3shft  11416  cjap  11484  caucvgrelemcau  11558  cvg1nlemcau  11562  cvg1nlemres  11563  recvguniq  11573  resqrexlemdecn  11590  resqrexlemcalc3  11594  resqrexlemcvg  11597  resqrexlemoverl  11599  leabs  11652  absexpzap  11658  ltabs  11665  abslt  11666  absle  11667  maxleim  11783  maxabslemval  11786  fimaxre2  11805  minmax  11808  2zinfmin  11821  xrmaxiflemcl  11823  xrmaxifle  11824  xrmaxiflemab  11825  xrmaxiflemlub  11826  xrmaxiflemcom  11827  xrmaxltsup  11836  xrmaxadd  11839  xrminmax  11843  xrbdtri  11854  2clim  11879  climshftlemg  11880  climsqz  11913  climsqz2  11914  climrecvg1n  11926  climcvg1nlem  11927  serf0  11930  sumrbdclem  11956  fsum3cvg  11957  summodclem3  11959  summodclem2a  11960  summodclem2  11961  zsumdc  11963  fsum3  11966  isumss  11970  fisumss  11971  fsum3cvg3  11975  fsumcl2lem  11977  fsumadd  11985  fsumsplit  11986  sumsnf  11988  fsum2d  12014  fisum0diag2  12026  fsummulc2  12027  modfsummod  12037  fsumabs  12044  fsumrelem  12050  fsumiun  12056  geoisumr  12097  cvgratnnlemseq  12105  cvgratz  12111  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  prodrbdclem  12150  fproddccvg  12151  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  fprodntrivap  12163  fprodssdc  12169  fprodmul  12170  prodsnf  12171  fprodsplitdc  12175  fprodsplit  12176  fprodunsn  12183  fprodcl2lem  12184  fprodap0  12200  fprod2d  12202  fprodrec  12208  fprodap0f  12215  efcj  12252  efaddlem  12253  tanaddaplem  12317  sinltxirr  12340  nndivides  12376  dvdsext  12434  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  bitsfzolem  12533  bitsmod  12535  bitsinv1  12541  dvdsbnd  12545  bezoutlemnewy  12585  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlemzz  12591  bezoutlemaz  12592  bezoutlembz  12593  bezoutlemeu  12596  bezoutlemle  12597  bezoutlemsup  12598  dfgcd3  12599  dfgcd2  12603  bezoutr1  12622  nnmindc  12623  nninfctlemfo  12629  dvdslcm  12659  lcmgcdlem  12667  qredeq  12686  qredeu  12687  divgcdcoprm0  12691  divgcdcoprmex  12692  cncongr1  12693  isprm2lem  12706  prmind2  12710  exprmfct  12728  prmdvdsfz  12729  isprm5lem  12731  prmexpb  12741  rpexp1i  12744  sqrt2irr  12752  sqne2sq  12767  nonsq  12797  phiprmpw  12812  eulerthlemrprm  12819  eulerthlema  12820  hashgcdeq  12830  phisum  12831  modprmn0modprm0  12847  pclemub  12878  pclemdc  12879  pcmul  12892  pcqmul  12894  pcxqcl  12903  pcdvdstr  12918  pcprmpw2  12924  difsqpwdvds  12929  pcmpt  12934  oddprmdvds  12945  prmpwdvds  12946  pockthg  12948  infpnlem1  12950  1arith  12958  4sqlem2  12980  4sqlemafi  12986  4sqlemffi  12987  4sqleminfi  12988  4sqlem11  12992  4sqlem13m  12994  4sqlem14  12995  4sqlem17  12998  4sqlem18  12999  ennnfonelemg  13042  ennnfoneleminc  13050  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemfun  13056  ennnfonelemf1  13057  ennnfonelemrn  13058  ennnfonelemdm  13059  ennnfonelemnn0  13061  ennnfonelemim  13063  exmidunben  13065  ctinfomlemom  13066  ctinf  13069  ctiunctlemudc  13076  nninfdclemlt  13090  nninfdclemf1  13091  isstruct2r  13111  prdsval  13374  imasival  13407  gsumpropd2  13494  sgrppropd  13514  prdssgrpd  13516  mndpropd  13541  issubmnd  13543  prdsidlem  13548  prdsmndd  13549  pws0g  13552  mndissubm  13576  resmhm2b  13590  mhmeql  13593  gsumfzz  13596  gsumwsubmcl  13597  gsumwmhm  13599  gsumfzcl  13600  grpinvnz  13672  pwssub  13714  mhmmnd  13721  mulgfng  13729  mulgz  13755  mulgnndir  13756  mulgnn0dir  13757  mulgneg2  13761  mulgass  13764  mhmmulg  13768  issubgrpd2  13795  issubg4m  13798  grpissubg  13799  isnsg3  13812  ghmpreima  13871  ghmnsgpreima  13874  ghmf1  13878  conjnmz  13884  conjnmzb  13885  eqgabl  13935  gsumfzreidx  13942  gsumfzsubmcl  13943  gsumfzmptfidmadd  13944  gsumfzmhm  13948  rngpropd  13987  issrg  13997  ringpropd  14070  ringinvnz1ne0  14081  dvdsrvald  14126  dvdsrd  14127  dvdsrtr  14134  unitgrp  14149  rhmopp  14209  lmodfopne  14359  lmodprop2d  14381  lssvacl  14398  lsslss  14414  lss1d  14416  lsspropdg  14464  rnglidlmcl  14513  lidlacl  14517  isridl  14537  znidomb  14691  znunit  14692  znrrg  14693  psrval  14699  mplsubgfilemcl  14732  mplsubgfileminv  14733  mplsubgfi  14734  tgdom  14815  neipsm  14897  tgrest  14912  cnfval  14937  cnpfval  14938  cnpval  14941  iscnp4  14961  cnpnei  14962  cnptopco  14965  cncnpi  14971  cncnp  14973  cnptopresti  14981  cnptoprest2  14983  cndis  14984  lmtopcnp  14993  txbasval  15010  neitx  15011  txcnp  15014  txcnmpt  15016  txcn  15018  imasnopn  15042  psmetres2  15076  isxmet2d  15091  xblss2ps  15147  xblss2  15148  blbas  15176  neibl  15234  metss2lem  15240  metrest  15249  xmettx  15253  metcnp3  15254  metcnp  15255  metcnp2  15256  metcnpi  15258  metcnpi2  15259  mulc1cncf  15332  cncfco  15334  mulcncflem  15350  mulcncf  15351  dedekindeulemuub  15360  dedekindeulemloc  15362  dedekindeulemlu  15364  dedekindeu  15366  suplociccreex  15367  suplociccex  15368  dedekindicclemuub  15369  dedekindicclemloc  15371  dedekindicclemlu  15373  dedekindicclemicc  15375  dedekindicc  15376  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemloc  15384  ivthinc  15386  limcimolemlt  15407  limccnp2lem  15419  limccnp2cntop  15420  limccoap  15421  dvcj  15452  dvmptfsum  15468  dveflem  15469  plyf  15480  plyaddlem1  15490  plymullem1  15491  plycolemc  15501  plyco  15502  plycj  15504  dvply1  15508  dvply2g  15509  efltlemlt  15517  sin0pilem1  15524  sin0pilem2  15525  pilem3  15526  coseq0negpitopi  15579  abssinper  15589  cos02pilt1  15594  relogeftb  15608  logbgcd1irraplemexp  15711  logbgcd1irrap  15713  dvdsppwf1o  15732  mpodvdsmulf1o  15733  mersenne  15740  perfectlem2  15743  perfect  15744  lgsval  15752  lgsfvalg  15753  lgsfcl2  15754  lgsval2lem  15758  lgsmod  15774  lgsdilem  15775  lgsdir2lem4  15779  lgsdir2  15781  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem2  15830  2lgslem1a1  15834  2lgslem1a  15836  2sqlem5  15867  2sqlem6  15868  2sqlem7  15869  2sqlem9  15872  2sqlem10  15873  umgrnloopv  15984  uhgr2edg  16076  upgredginwlk  16226  clwwlkccatlem  16270  eupth2lem3lem3fi  16340  eupth2lem3lem4fi  16343  eupth2lemsfi  16348  depindlem3  16378  bj-findis  16625  2omap  16645  pwle2  16650  pwf1oexmid  16651  pw1nct  16655  nnsf  16658  peano4nninf  16659  nninfall  16662  nninfsellemeq  16667  nninfsellemeqinf  16669  nnnninfex  16675  nninfnfiinf  16676  qdencn  16682  refeq  16683  trilpolemeq1  16695  trilpolemlt1  16696  trirec0  16699  nconstwlpolemgt0  16720  nconstwlpolem  16721  neapmkvlem  16723  gfsumval  16732  gfsumcl  16739