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  vtoclgft  2787  reupick  3419  euotd  4254  frirrg  4350  ralxfrd  4462  nnsucpred  4616  foun  5480  f1oprg  5505  dffo4  5664  foeqcnvco  5790  fliftfun  5796  isotr  5816  riotass2  5856  ovmpodxf  5999  mpoxopoveq  6240  tfrlem1  6308  tfrlemibacc  6326  tfrlemibfn  6328  tfrlemi14d  6333  tfrexlem  6334  tfr1onlembacc  6342  tfr1onlembfn  6344  tfr1onlemres  6349  tfrcllembacc  6355  tfrcllembfn  6357  tfrcllemres  6362  frecabcl  6399  nnmordi  6516  eroprf  6627  f1imaen2g  6792  xpen  6844  mapen  6845  mapdom1g  6846  mapxpen  6847  xpmapenlem  6848  phplem4dom  6861  nndomo  6863  phpm  6864  fidifsnen  6869  dif1enen  6879  fisbth  6882  fimax2gtrilemstep  6899  fimax2gtri  6900  en2eqpr  6906  unsnfidcex  6918  unsnfidcel  6919  ssfirab  6932  fidcenumlemrks  6951  sbthlemi8  6962  fiuni  6976  ordiso2  7033  updjud  7080  difinfsnlem  7097  ctssdclemn0  7108  ctssdccl  7109  ctssdc  7111  enumctlemm  7112  enumct  7113  nnnninfeq  7125  nninfisol  7130  enomnilem  7135  fodju0  7144  enmkvlem  7158  enwomnilem  7166  nninfwlpoimlemg  7172  exmidfodomrlemim  7199  exmidontriimlem2  7220  exmidapne  7258  cc3  7266  dfplpq2  7352  nqpi  7376  nqnq0pi  7436  nq0nn  7440  elinp  7472  elnp1st2nd  7474  genprndl  7519  genprndu  7520  addnqprllem  7525  addnqprulem  7526  addnqprl  7527  addnqpru  7528  addlocpr  7534  nqprloc  7543  prmuloc  7564  mulnqprl  7566  mulnqpru  7567  mullocpr  7569  distrlem1prl  7580  distrlem1pru  7581  ltsopr  7594  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemloc  7605  ltexprlemrl  7608  ltexprlemru  7610  addcanprleml  7612  addcanprlemu  7613  recexprlemloc  7629  recexprlem1ssl  7631  recexprlem1ssu  7632  aptiprleml  7637  aptiprlemu  7638  archpr  7641  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlemladdru  7654  archrecpr  7662  caucvgprlemnkj  7664  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemladdfu  7675  caucvgprprlemnkltj  7687  caucvgprprlemnkeqj  7688  caucvgprprlemnjltk  7689  caucvgprprlemml  7692  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemdisj  7700  caucvgprprlemexbt  7704  caucvgprprlemexb  7705  caucvgprprlemaddq  7706  suplocexprlemru  7717  suplocexprlemloc  7719  suplocexprlemex  7720  suplocexprlemub  7721  suplocexprlemlub  7722  mulgt0sr  7776  caucvgsrlemcau  7791  caucvgsrlemoffcau  7796  caucvgsrlemoffres  7798  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  axcaucvglemcau  7896  axcaucvglemres  7897  axpre-suploclemres  7899  axsuploc  8029  cnegexlem1  8131  cnegex  8134  apsym  8562  apcotr  8563  apadd1  8564  mulext1  8568  mulge0  8575  apti  8578  aprcl  8602  conjmulap  8685  lemulge11  8822  creui  8916  nndiv  8959  zaddcllemneg  9291  suprzclex  9350  eluzuzle  9535  infregelbex  9597  divfnzn  9620  qapne  9638  xrltso  9795  xnn0dcle  9801  xnn0letri  9802  xrre  9819  xrre3  9821  xaddf  9843  xaddval  9844  xpncan  9870  xleadd1a  9872  xltadd1  9875  xleaddadd  9886  ixxss12  9905  elioc2  9935  elico2  9936  elicc2  9937  fzm1  10099  fzneuz  10100  eluzgtdifelfzo  10196  elfzonelfzo  10229  exfzdc  10239  qtri3or  10242  exbtwnzlemstep  10247  exbtwnzlemex  10249  exbtwnz  10250  modqid  10348  modqcyc2  10359  modqmuladd  10365  modqmuladdnn0  10367  modaddmodlo  10387  addmodlteq  10397  frecuzrdgrrn  10407  frec2uzrdg  10408  frecuzrdgsuc  10413  frecuzrdgsuctlem  10422  seq3clss  10466  iseqf1olemqcl  10485  iseqf1olemnab  10487  iseqf1olemab  10488  iseqf1olemmo  10491  iseqf1olemqf1o  10492  iseqf1olemjpcl  10494  iseqf1olemqpcl  10495  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3f1olemp  10501  seq3f1oleml  10502  seq3f1o  10503  seq3id3  10506  ser3ge0  10516  exp3val  10521  expap0  10549  qsqeqor  10630  modqexp  10646  nn0ltexp2  10688  facndiv  10718  faclbnd  10720  bcval5  10742  hashunlem  10783  hashun  10784  hashprg  10787  fiprsshashgt1  10796  hashfacen  10815  zfz1isolemiso  10818  zfz1isolem1  10819  seq3coll  10821  ovshftex  10827  2shfti  10839  seq3shft  10846  cjap  10914  caucvgrelemcau  10988  cvg1nlemcau  10992  cvg1nlemres  10993  recvguniq  11003  resqrexlemdecn  11020  resqrexlemcalc3  11024  resqrexlemcvg  11027  resqrexlemoverl  11029  leabs  11082  absexpzap  11088  ltabs  11095  abslt  11096  absle  11097  maxleim  11213  maxabslemval  11216  fimaxre2  11234  minmax  11237  2zinfmin  11250  xrmaxiflemcl  11252  xrmaxifle  11253  xrmaxiflemab  11254  xrmaxiflemlub  11255  xrmaxiflemcom  11256  xrmaxltsup  11265  xrmaxadd  11268  xrminmax  11272  xrbdtri  11283  2clim  11308  climshftlemg  11309  climsqz  11342  climsqz2  11343  climrecvg1n  11355  climcvg1nlem  11356  serf0  11359  sumrbdclem  11384  fsum3cvg  11385  summodclem3  11387  summodclem2a  11388  summodclem2  11389  zsumdc  11391  fsum3  11394  isumss  11398  fisumss  11399  fsum3cvg3  11403  fsumcl2lem  11405  fsumadd  11413  fsumsplit  11414  sumsnf  11416  fsum2d  11442  fisum0diag2  11454  fsummulc2  11455  modfsummod  11465  fsumabs  11472  fsumrelem  11478  fsumiun  11484  geoisumr  11525  cvgratnnlemseq  11533  cvgratz  11539  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  prodrbdclem  11578  fproddccvg  11579  prodmodclem3  11582  prodmodclem2a  11583  zproddc  11586  fprodseq  11590  fprodntrivap  11591  fprodssdc  11597  fprodmul  11598  prodsnf  11599  fprodsplitdc  11603  fprodsplit  11604  fprodunsn  11611  fprodcl2lem  11612  fprodap0  11628  fprod2d  11630  fprodrec  11636  fprodap0f  11643  efcj  11680  efaddlem  11681  tanaddaplem  11745  nndivides  11803  dvdsext  11860  divalglemeunn  11925  divalglemex  11926  divalglemeuneg  11927  zsupcllemstep  11945  infssuzex  11949  suprzubdc  11952  nninfdcex  11953  zsupssdc  11954  dvdsbnd  11956  bezoutlemnewy  11996  bezoutlemstep  11997  bezoutlemmain  11998  bezoutlemzz  12002  bezoutlemaz  12003  bezoutlembz  12004  bezoutlemeu  12007  bezoutlemle  12008  bezoutlemsup  12009  dfgcd3  12010  dfgcd2  12014  bezoutr1  12033  nnmindc  12034  dvdslcm  12068  lcmgcdlem  12076  qredeq  12095  qredeu  12096  divgcdcoprm0  12100  divgcdcoprmex  12101  cncongr1  12102  isprm2lem  12115  prmind2  12119  exprmfct  12137  prmdvdsfz  12138  isprm5lem  12140  prmexpb  12150  rpexp1i  12153  sqrt2irr  12161  sqne2sq  12176  nonsq  12206  phiprmpw  12221  eulerthlemrprm  12228  eulerthlema  12229  hashgcdeq  12238  phisum  12239  modprmn0modprm0  12255  pclemub  12286  pclemdc  12287  pcmul  12300  pcqmul  12302  pcdvdstr  12325  pcprmpw2  12331  difsqpwdvds  12336  pcmpt  12340  oddprmdvds  12351  prmpwdvds  12352  pockthg  12354  infpnlem1  12356  1arith  12364  4sqlem2  12386  ennnfonelemg  12403  ennnfoneleminc  12411  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemex  12414  ennnfonelemhom  12415  ennnfonelemfun  12417  ennnfonelemf1  12418  ennnfonelemrn  12419  ennnfonelemdm  12420  ennnfonelemnn0  12422  ennnfonelemim  12424  exmidunben  12426  ctinfomlemom  12427  ctinf  12430  ctiunctlemudc  12437  nninfdclemlt  12451  nninfdclemf1  12452  isstruct2r  12472  imasival  12726  mndpropd  12840  issubmnd  12842  mndissubm  12865  mhmeql  12875  grpinvnz  12940  mhmmnd  12979  mulgfng  12986  mulgz  13009  mulgnndir  13010  mulgnn0dir  13011  mulgneg2  13015  mulgass  13018  mhmmulg  13022  issubgrpd2  13048  issubg4m  13051  grpissubg  13052  isnsg3  13065  issrg  13146  ringpropd  13215  ringinvnz1ne0  13224  dvdsrvald  13260  dvdsrd  13261  dvdsrtr  13268  unitgrp  13283  tgdom  13542  neipsm  13624  tgrest  13639  cnfval  13664  cnpfval  13665  cnpval  13668  iscnp4  13688  cnpnei  13689  cnptopco  13692  cncnpi  13698  cncnp  13700  cnptopresti  13708  cnptoprest2  13710  cndis  13711  lmtopcnp  13720  txbasval  13737  neitx  13738  txcnp  13741  txcnmpt  13743  txcn  13745  imasnopn  13769  psmetres2  13803  isxmet2d  13818  xblss2ps  13874  xblss2  13875  blbas  13903  neibl  13961  metss2lem  13967  metrest  13976  xmettx  13980  metcnp3  13981  metcnp  13982  metcnp2  13983  metcnpi  13985  metcnpi2  13986  mulc1cncf  14046  cncfco  14048  mulcncflem  14060  mulcncf  14061  dedekindeulemuub  14065  dedekindeulemloc  14067  dedekindeulemlu  14069  dedekindeu  14071  suplociccreex  14072  suplociccex  14073  dedekindicclemuub  14074  dedekindicclemloc  14076  dedekindicclemlu  14078  dedekindicclemicc  14080  dedekindicc  14081  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemloc  14089  ivthinc  14091  limcimolemlt  14103  limccnp2lem  14115  limccnp2cntop  14116  limccoap  14117  dvcj  14143  dveflem  14157  efltlemlt  14165  sin0pilem1  14172  sin0pilem2  14173  pilem3  14174  coseq0negpitopi  14227  abssinper  14237  cos02pilt1  14242  relogeftb  14256  logbgcd1irraplemexp  14356  logbgcd1irrap  14358  lgsval  14375  lgsfvalg  14376  lgsfcl2  14377  lgsval2lem  14381  lgsmod  14397  lgsdilem  14398  lgsdir2lem4  14402  lgsdir2  14404  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgsdirnn0  14418  lgsdinn0  14419  2sqlem5  14436  2sqlem6  14437  2sqlem7  14438  2sqlem9  14441  2sqlem10  14442  bj-findis  14701  pwle2  14718  pwf1oexmid  14719  pw1nct  14722  nnsf  14724  peano4nninf  14725  nninfall  14728  nninfsellemeq  14733  nninfsellemeqinf  14735  qdencn  14745  refeq  14746  trilpolemeq1  14758  trilpolemlt1  14759  trirec0  14762  nconstwlpolemgt0  14781  nconstwlpolem  14782  neapmkvlem  14784