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  2814  reupick  3448  euotd  4288  frirrg  4386  ralxfrd  4498  nnsucpred  4654  foun  5526  f1oprg  5551  dffo4  5713  foeqcnvco  5840  fliftfun  5846  isotr  5866  riotass2  5907  ovmpodxf  6052  mpoxopoveq  6307  tfrlem1  6375  tfrlemibacc  6393  tfrlemibfn  6395  tfrlemi14d  6400  tfrexlem  6401  tfr1onlembacc  6409  tfr1onlembfn  6411  tfr1onlemres  6416  tfrcllembacc  6422  tfrcllembfn  6424  tfrcllemres  6429  frecabcl  6466  nnmordi  6583  eroprf  6696  f1imaen2g  6861  pw2f1odclem  6904  xpen  6915  mapen  6916  mapdom1g  6917  mapxpen  6918  xpmapenlem  6919  phplem4dom  6932  nndomo  6934  phpm  6935  fidifsnen  6940  dif1enen  6950  fisbth  6953  fimax2gtrilemstep  6970  fimax2gtri  6971  en2eqpr  6977  unsnfidcex  6990  unsnfidcel  6991  ssfirab  7006  fidcenumlemrks  7028  sbthlemi8  7039  fiuni  7053  ordiso2  7110  updjud  7157  difinfsnlem  7174  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  enumct  7190  nnnninfeq  7203  nninfisol  7208  enomnilem  7213  fodju0  7222  enmkvlem  7236  enwomnilem  7244  nninfwlpoimlemg  7250  exmidfodomrlemim  7280  exmidontriimlem2  7305  exmidapne  7343  cc3  7351  dfplpq2  7438  nqpi  7462  nqnq0pi  7522  nq0nn  7526  elinp  7558  elnp1st2nd  7560  genprndl  7605  genprndu  7606  addnqprllem  7611  addnqprulem  7612  addnqprl  7613  addnqpru  7614  addlocpr  7620  nqprloc  7629  prmuloc  7650  mulnqprl  7652  mulnqpru  7653  mullocpr  7655  distrlem1prl  7666  distrlem1pru  7667  ltsopr  7680  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemloc  7691  ltexprlemrl  7694  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  recexprlemloc  7715  recexprlem1ssl  7717  recexprlem1ssu  7718  aptiprleml  7723  aptiprlemu  7724  archpr  7727  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  archrecpr  7748  caucvgprlemnkj  7750  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemladdfu  7761  caucvgprprlemnkltj  7773  caucvgprprlemnkeqj  7774  caucvgprprlemnjltk  7775  caucvgprprlemml  7778  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemdisj  7786  caucvgprprlemexbt  7790  caucvgprprlemexb  7791  caucvgprprlemaddq  7792  suplocexprlemru  7803  suplocexprlemloc  7805  suplocexprlemex  7806  suplocexprlemub  7807  suplocexprlemlub  7808  mulgt0sr  7862  caucvgsrlemcau  7877  caucvgsrlemoffcau  7882  caucvgsrlemoffres  7884  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  axcaucvglemcau  7982  axcaucvglemres  7983  axpre-suploclemres  7985  axsuploc  8116  cnegexlem1  8218  cnegex  8221  apsym  8650  apcotr  8651  apadd1  8652  mulext1  8656  mulge0  8663  apti  8666  aprcl  8690  conjmulap  8773  lemulge11  8910  creui  9004  nndiv  9048  zaddcllemneg  9382  suprzclex  9441  eluzuzle  9626  infregelbex  9689  divfnzn  9712  qapne  9730  xrltso  9888  xnn0dcle  9894  xnn0letri  9895  xrre  9912  xrre3  9914  xaddf  9936  xaddval  9937  xpncan  9963  xleadd1a  9965  xltadd1  9968  xleaddadd  9979  ixxss12  9998  elioc2  10028  elico2  10029  elicc2  10030  fzm1  10192  fzneuz  10193  eluzgtdifelfzo  10290  elfzonelfzo  10323  exfzdc  10333  zsupcllemstep  10336  infssuzex  10340  suprzubdc  10343  nninfdcex  10344  zsupssdc  10345  qtri3or  10347  exbtwnzlemstep  10354  exbtwnzlemex  10356  exbtwnz  10357  modqid  10458  modqcyc2  10469  modqmuladd  10475  modqmuladdnn0  10477  modaddmodlo  10497  addmodlteq  10507  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdgsuc  10523  frecuzrdgsuctlem  10532  nninfinf  10552  seq3clss  10580  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemab  10611  iseqf1olemmo  10614  iseqf1olemqf1o  10615  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seq3f1olemp  10624  seq3f1oleml  10625  seq3f1o  10626  seqf1oglem1  10628  seqf1oglem2  10629  seqf1og  10630  seq3id3  10633  seqfeq4g  10640  ser3ge0  10645  exp3val  10650  expap0  10678  qsqeqor  10759  modqexp  10775  nn0ltexp2  10818  facndiv  10848  faclbnd  10850  bcval5  10872  hashunlem  10913  hashun  10914  hashprg  10917  fiprsshashgt1  10926  hashfacen  10945  zfz1isolemiso  10948  zfz1isolem1  10949  seq3coll  10951  ovshftex  11001  2shfti  11013  seq3shft  11020  cjap  11088  caucvgrelemcau  11162  cvg1nlemcau  11166  cvg1nlemres  11167  recvguniq  11177  resqrexlemdecn  11194  resqrexlemcalc3  11198  resqrexlemcvg  11201  resqrexlemoverl  11203  leabs  11256  absexpzap  11262  ltabs  11269  abslt  11270  absle  11271  maxleim  11387  maxabslemval  11390  fimaxre2  11409  minmax  11412  2zinfmin  11425  xrmaxiflemcl  11427  xrmaxifle  11428  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxiflemcom  11431  xrmaxltsup  11440  xrmaxadd  11443  xrminmax  11447  xrbdtri  11458  2clim  11483  climshftlemg  11484  climsqz  11517  climsqz2  11518  climrecvg1n  11530  climcvg1nlem  11531  serf0  11534  sumrbdclem  11559  fsum3cvg  11560  summodclem3  11562  summodclem2a  11563  summodclem2  11564  zsumdc  11566  fsum3  11569  isumss  11573  fisumss  11574  fsum3cvg3  11578  fsumcl2lem  11580  fsumadd  11588  fsumsplit  11589  sumsnf  11591  fsum2d  11617  fisum0diag2  11629  fsummulc2  11630  modfsummod  11640  fsumabs  11647  fsumrelem  11653  fsumiun  11659  geoisumr  11700  cvgratnnlemseq  11708  cvgratz  11714  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodrbdclem  11753  fproddccvg  11754  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  fprodntrivap  11766  fprodssdc  11772  fprodmul  11773  prodsnf  11774  fprodsplitdc  11778  fprodsplit  11779  fprodunsn  11786  fprodcl2lem  11787  fprodap0  11803  fprod2d  11805  fprodrec  11811  fprodap0f  11818  efcj  11855  efaddlem  11856  tanaddaplem  11920  sinltxirr  11943  nndivides  11979  dvdsext  12037  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  bitsfzolem  12136  bitsmod  12138  bitsinv1  12144  dvdsbnd  12148  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlemzz  12194  bezoutlemaz  12195  bezoutlembz  12196  bezoutlemeu  12199  bezoutlemle  12200  bezoutlemsup  12201  dfgcd3  12202  dfgcd2  12206  bezoutr1  12225  nnmindc  12226  nninfctlemfo  12232  dvdslcm  12262  lcmgcdlem  12270  qredeq  12289  qredeu  12290  divgcdcoprm0  12294  divgcdcoprmex  12295  cncongr1  12296  isprm2lem  12309  prmind2  12313  exprmfct  12331  prmdvdsfz  12332  isprm5lem  12334  prmexpb  12344  rpexp1i  12347  sqrt2irr  12355  sqne2sq  12370  nonsq  12400  phiprmpw  12415  eulerthlemrprm  12422  eulerthlema  12423  hashgcdeq  12433  phisum  12434  modprmn0modprm0  12450  pclemub  12481  pclemdc  12482  pcmul  12495  pcqmul  12497  pcxqcl  12506  pcdvdstr  12521  pcprmpw2  12527  difsqpwdvds  12532  pcmpt  12537  oddprmdvds  12548  prmpwdvds  12549  pockthg  12551  infpnlem1  12553  1arith  12561  4sqlem2  12583  4sqlemafi  12589  4sqlemffi  12590  4sqleminfi  12591  4sqlem11  12595  4sqlem13m  12597  4sqlem14  12598  4sqlem17  12601  4sqlem18  12602  ennnfonelemg  12645  ennnfoneleminc  12653  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemfun  12659  ennnfonelemf1  12660  ennnfonelemrn  12661  ennnfonelemdm  12662  ennnfonelemnn0  12664  ennnfonelemim  12666  exmidunben  12668  ctinfomlemom  12669  ctinf  12672  ctiunctlemudc  12679  nninfdclemlt  12693  nninfdclemf1  12694  isstruct2r  12714  prdsval  12975  imasival  13008  gsumpropd2  13095  sgrppropd  13115  prdssgrpd  13117  mndpropd  13142  issubmnd  13144  prdsidlem  13149  prdsmndd  13150  pws0g  13153  mndissubm  13177  resmhm2b  13191  mhmeql  13194  gsumfzz  13197  gsumwsubmcl  13198  gsumwmhm  13200  gsumfzcl  13201  grpinvnz  13273  pwssub  13315  mhmmnd  13322  mulgfng  13330  mulgz  13356  mulgnndir  13357  mulgnn0dir  13358  mulgneg2  13362  mulgass  13365  mhmmulg  13369  issubgrpd2  13396  issubg4m  13399  grpissubg  13400  isnsg3  13413  ghmpreima  13472  ghmnsgpreima  13475  ghmf1  13479  conjnmz  13485  conjnmzb  13486  eqgabl  13536  gsumfzreidx  13543  gsumfzsubmcl  13544  gsumfzmptfidmadd  13545  gsumfzmhm  13549  rngpropd  13587  issrg  13597  ringpropd  13670  ringinvnz1ne0  13681  dvdsrvald  13725  dvdsrd  13726  dvdsrtr  13733  unitgrp  13748  rhmopp  13808  lmodfopne  13958  lmodprop2d  13980  lssvacl  13997  lsslss  14013  lss1d  14015  lsspropdg  14063  rnglidlmcl  14112  lidlacl  14116  isridl  14136  znidomb  14290  znunit  14291  znrrg  14292  psrval  14296  tgdom  14392  neipsm  14474  tgrest  14489  cnfval  14514  cnpfval  14515  cnpval  14518  iscnp4  14538  cnpnei  14539  cnptopco  14542  cncnpi  14548  cncnp  14550  cnptopresti  14558  cnptoprest2  14560  cndis  14561  lmtopcnp  14570  txbasval  14587  neitx  14588  txcnp  14591  txcnmpt  14593  txcn  14595  imasnopn  14619  psmetres2  14653  isxmet2d  14668  xblss2ps  14724  xblss2  14725  blbas  14753  neibl  14811  metss2lem  14817  metrest  14826  xmettx  14830  metcnp3  14831  metcnp  14832  metcnp2  14833  metcnpi  14835  metcnpi2  14836  mulc1cncf  14909  cncfco  14911  mulcncflem  14927  mulcncf  14928  dedekindeulemuub  14937  dedekindeulemloc  14939  dedekindeulemlu  14941  dedekindeu  14943  suplociccreex  14944  suplociccex  14945  dedekindicclemuub  14946  dedekindicclemloc  14948  dedekindicclemlu  14950  dedekindicclemicc  14952  dedekindicc  14953  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemloc  14961  ivthinc  14963  limcimolemlt  14984  limccnp2lem  14996  limccnp2cntop  14997  limccoap  14998  dvcj  15029  dvmptfsum  15045  dveflem  15046  plyf  15057  plyaddlem1  15067  plymullem1  15068  plycolemc  15078  plyco  15079  plycj  15081  dvply1  15085  dvply2g  15086  efltlemlt  15094  sin0pilem1  15101  sin0pilem2  15102  pilem3  15103  coseq0negpitopi  15156  abssinper  15166  cos02pilt1  15171  relogeftb  15185  logbgcd1irraplemexp  15288  logbgcd1irrap  15290  dvdsppwf1o  15309  mpodvdsmulf1o  15310  mersenne  15317  perfectlem2  15320  perfect  15321  lgsval  15329  lgsfvalg  15330  lgsfcl2  15331  lgsval2lem  15335  lgsmod  15351  lgsdilem  15352  lgsdir2lem4  15356  lgsdir2  15358  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem2  15407  2lgslem1a1  15411  2lgslem1a  15413  2sqlem5  15444  2sqlem6  15445  2sqlem7  15446  2sqlem9  15449  2sqlem10  15450  bj-findis  15709  2omap  15726  pwle2  15729  pwf1oexmid  15730  pw1nct  15734  nnsf  15736  peano4nninf  15737  nninfall  15740  nninfsellemeq  15745  nninfsellemeqinf  15747  qdencn  15758  refeq  15759  trilpolemeq1  15771  trilpolemlt1  15772  trirec0  15775  nconstwlpolemgt0  15795  nconstwlpolem  15796  neapmkvlem  15798