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  2810  reupick  3443  euotd  4283  frirrg  4381  ralxfrd  4493  nnsucpred  4649  foun  5519  f1oprg  5544  dffo4  5706  foeqcnvco  5833  fliftfun  5839  isotr  5859  riotass2  5900  ovmpodxf  6044  mpoxopoveq  6293  tfrlem1  6361  tfrlemibacc  6379  tfrlemibfn  6381  tfrlemi14d  6386  tfrexlem  6387  tfr1onlembacc  6395  tfr1onlembfn  6397  tfr1onlemres  6402  tfrcllembacc  6408  tfrcllembfn  6410  tfrcllemres  6415  frecabcl  6452  nnmordi  6569  eroprf  6682  f1imaen2g  6847  pw2f1odclem  6890  xpen  6901  mapen  6902  mapdom1g  6903  mapxpen  6904  xpmapenlem  6905  phplem4dom  6918  nndomo  6920  phpm  6921  fidifsnen  6926  dif1enen  6936  fisbth  6939  fimax2gtrilemstep  6956  fimax2gtri  6957  en2eqpr  6963  unsnfidcex  6976  unsnfidcel  6977  ssfirab  6990  fidcenumlemrks  7012  sbthlemi8  7023  fiuni  7037  ordiso2  7094  updjud  7141  difinfsnlem  7158  ctssdclemn0  7169  ctssdccl  7170  ctssdc  7172  enumctlemm  7173  enumct  7174  nnnninfeq  7187  nninfisol  7192  enomnilem  7197  fodju0  7206  enmkvlem  7220  enwomnilem  7228  nninfwlpoimlemg  7234  exmidfodomrlemim  7261  exmidontriimlem2  7282  exmidapne  7320  cc3  7328  dfplpq2  7414  nqpi  7438  nqnq0pi  7498  nq0nn  7502  elinp  7534  elnp1st2nd  7536  genprndl  7581  genprndu  7582  addnqprllem  7587  addnqprulem  7588  addnqprl  7589  addnqpru  7590  addlocpr  7596  nqprloc  7605  prmuloc  7626  mulnqprl  7628  mulnqpru  7629  mullocpr  7631  distrlem1prl  7642  distrlem1pru  7643  ltsopr  7656  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemloc  7667  ltexprlemrl  7670  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  recexprlemloc  7691  recexprlem1ssl  7693  recexprlem1ssu  7694  aptiprleml  7699  aptiprlemu  7700  archpr  7703  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  archrecpr  7724  caucvgprlemnkj  7726  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemladdfu  7737  caucvgprprlemnkltj  7749  caucvgprprlemnkeqj  7750  caucvgprprlemnjltk  7751  caucvgprprlemml  7754  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemdisj  7762  caucvgprprlemexbt  7766  caucvgprprlemexb  7767  caucvgprprlemaddq  7768  suplocexprlemru  7779  suplocexprlemloc  7781  suplocexprlemex  7782  suplocexprlemub  7783  suplocexprlemlub  7784  mulgt0sr  7838  caucvgsrlemcau  7853  caucvgsrlemoffcau  7858  caucvgsrlemoffres  7860  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  axcaucvglemcau  7958  axcaucvglemres  7959  axpre-suploclemres  7961  axsuploc  8092  cnegexlem1  8194  cnegex  8197  apsym  8625  apcotr  8626  apadd1  8627  mulext1  8631  mulge0  8638  apti  8641  aprcl  8665  conjmulap  8748  lemulge11  8885  creui  8979  nndiv  9023  zaddcllemneg  9356  suprzclex  9415  eluzuzle  9600  infregelbex  9663  divfnzn  9686  qapne  9704  xrltso  9862  xnn0dcle  9868  xnn0letri  9869  xrre  9886  xrre3  9888  xaddf  9910  xaddval  9911  xpncan  9937  xleadd1a  9939  xltadd1  9942  xleaddadd  9953  ixxss12  9972  elioc2  10002  elico2  10003  elicc2  10004  fzm1  10166  fzneuz  10167  eluzgtdifelfzo  10264  elfzonelfzo  10297  exfzdc  10307  qtri3or  10310  exbtwnzlemstep  10316  exbtwnzlemex  10318  exbtwnz  10319  modqid  10420  modqcyc2  10431  modqmuladd  10437  modqmuladdnn0  10439  modaddmodlo  10459  addmodlteq  10469  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgsuc  10485  frecuzrdgsuctlem  10494  nninfinf  10514  seq3clss  10542  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemab  10573  iseqf1olemmo  10576  iseqf1olemqf1o  10577  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seq3f1olemp  10586  seq3f1oleml  10587  seq3f1o  10588  seqf1oglem1  10590  seqf1oglem2  10591  seqf1og  10592  seq3id3  10595  seqfeq4g  10602  ser3ge0  10607  exp3val  10612  expap0  10640  qsqeqor  10721  modqexp  10737  nn0ltexp2  10780  facndiv  10810  faclbnd  10812  bcval5  10834  hashunlem  10875  hashun  10876  hashprg  10879  fiprsshashgt1  10888  hashfacen  10907  zfz1isolemiso  10910  zfz1isolem1  10911  seq3coll  10913  ovshftex  10963  2shfti  10975  seq3shft  10982  cjap  11050  caucvgrelemcau  11124  cvg1nlemcau  11128  cvg1nlemres  11129  recvguniq  11139  resqrexlemdecn  11156  resqrexlemcalc3  11160  resqrexlemcvg  11163  resqrexlemoverl  11165  leabs  11218  absexpzap  11224  ltabs  11231  abslt  11232  absle  11233  maxleim  11349  maxabslemval  11352  fimaxre2  11370  minmax  11373  2zinfmin  11386  xrmaxiflemcl  11388  xrmaxifle  11389  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxiflemcom  11392  xrmaxltsup  11401  xrmaxadd  11404  xrminmax  11408  xrbdtri  11419  2clim  11444  climshftlemg  11445  climsqz  11478  climsqz2  11479  climrecvg1n  11491  climcvg1nlem  11492  serf0  11495  sumrbdclem  11520  fsum3cvg  11521  summodclem3  11523  summodclem2a  11524  summodclem2  11525  zsumdc  11527  fsum3  11530  isumss  11534  fisumss  11535  fsum3cvg3  11539  fsumcl2lem  11541  fsumadd  11549  fsumsplit  11550  sumsnf  11552  fsum2d  11578  fisum0diag2  11590  fsummulc2  11591  modfsummod  11601  fsumabs  11608  fsumrelem  11614  fsumiun  11620  geoisumr  11661  cvgratnnlemseq  11669  cvgratz  11675  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodrbdclem  11714  fproddccvg  11715  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  fprodntrivap  11727  fprodssdc  11733  fprodmul  11734  prodsnf  11735  fprodsplitdc  11739  fprodsplit  11740  fprodunsn  11747  fprodcl2lem  11748  fprodap0  11764  fprod2d  11766  fprodrec  11772  fprodap0f  11779  efcj  11816  efaddlem  11817  tanaddaplem  11881  sinltxirr  11904  nndivides  11940  dvdsext  11997  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  zsupcllemstep  12082  infssuzex  12086  suprzubdc  12089  nninfdcex  12090  zsupssdc  12091  dvdsbnd  12093  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlemzz  12139  bezoutlemaz  12140  bezoutlembz  12141  bezoutlemeu  12144  bezoutlemle  12145  bezoutlemsup  12146  dfgcd3  12147  dfgcd2  12151  bezoutr1  12170  nnmindc  12171  nninfctlemfo  12177  dvdslcm  12207  lcmgcdlem  12215  qredeq  12234  qredeu  12235  divgcdcoprm0  12239  divgcdcoprmex  12240  cncongr1  12241  isprm2lem  12254  prmind2  12258  exprmfct  12276  prmdvdsfz  12277  isprm5lem  12279  prmexpb  12289  rpexp1i  12292  sqrt2irr  12300  sqne2sq  12315  nonsq  12345  phiprmpw  12360  eulerthlemrprm  12367  eulerthlema  12368  hashgcdeq  12377  phisum  12378  modprmn0modprm0  12394  pclemub  12425  pclemdc  12426  pcmul  12439  pcqmul  12441  pcxqcl  12450  pcdvdstr  12465  pcprmpw2  12471  difsqpwdvds  12476  pcmpt  12481  oddprmdvds  12492  prmpwdvds  12493  pockthg  12495  infpnlem1  12497  1arith  12505  4sqlem2  12527  4sqlemafi  12533  4sqlemffi  12534  4sqleminfi  12535  4sqlem11  12539  4sqlem13m  12541  4sqlem14  12542  4sqlem17  12545  4sqlem18  12546  ennnfonelemg  12560  ennnfoneleminc  12568  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemfun  12574  ennnfonelemf1  12575  ennnfonelemrn  12576  ennnfonelemdm  12577  ennnfonelemnn0  12579  ennnfonelemim  12581  exmidunben  12583  ctinfomlemom  12584  ctinf  12587  ctiunctlemudc  12594  nninfdclemlt  12608  nninfdclemf1  12609  isstruct2r  12629  imasival  12889  gsumpropd2  12976  sgrppropd  12996  mndpropd  13021  issubmnd  13023  mndissubm  13047  resmhm2b  13061  mhmeql  13064  gsumfzz  13067  gsumwsubmcl  13068  gsumwmhm  13070  gsumfzcl  13071  grpinvnz  13143  mhmmnd  13186  mulgfng  13194  mulgz  13220  mulgnndir  13221  mulgnn0dir  13222  mulgneg2  13226  mulgass  13229  mhmmulg  13233  issubgrpd2  13260  issubg4m  13263  grpissubg  13264  isnsg3  13277  ghmpreima  13336  ghmnsgpreima  13339  ghmf1  13343  conjnmz  13349  conjnmzb  13350  eqgabl  13400  gsumfzreidx  13407  gsumfzsubmcl  13408  gsumfzmptfidmadd  13409  gsumfzmhm  13413  rngpropd  13451  issrg  13461  ringpropd  13534  ringinvnz1ne0  13545  dvdsrvald  13589  dvdsrd  13590  dvdsrtr  13597  unitgrp  13612  rhmopp  13672  lmodfopne  13822  lmodprop2d  13844  lssvacl  13861  lsslss  13877  lss1d  13879  lsspropdg  13927  rnglidlmcl  13976  lidlacl  13980  isridl  14000  znidomb  14146  znunit  14147  znrrg  14148  psrval  14152  tgdom  14240  neipsm  14322  tgrest  14337  cnfval  14362  cnpfval  14363  cnpval  14366  iscnp4  14386  cnpnei  14387  cnptopco  14390  cncnpi  14396  cncnp  14398  cnptopresti  14406  cnptoprest2  14408  cndis  14409  lmtopcnp  14418  txbasval  14435  neitx  14436  txcnp  14439  txcnmpt  14441  txcn  14443  imasnopn  14467  psmetres2  14501  isxmet2d  14516  xblss2ps  14572  xblss2  14573  blbas  14601  neibl  14659  metss2lem  14665  metrest  14674  xmettx  14678  metcnp3  14679  metcnp  14680  metcnp2  14681  metcnpi  14683  metcnpi2  14684  mulc1cncf  14744  cncfco  14746  mulcncflem  14761  mulcncf  14762  dedekindeulemuub  14771  dedekindeulemloc  14773  dedekindeulemlu  14775  dedekindeu  14777  suplociccreex  14778  suplociccex  14779  dedekindicclemuub  14780  dedekindicclemloc  14782  dedekindicclemlu  14784  dedekindicclemicc  14786  dedekindicc  14787  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemloc  14795  ivthinc  14797  limcimolemlt  14818  limccnp2lem  14830  limccnp2cntop  14831  limccoap  14832  dvcj  14858  dveflem  14872  plyf  14883  plyaddlem1  14893  plymullem1  14894  efltlemlt  14909  sin0pilem1  14916  sin0pilem2  14917  pilem3  14918  coseq0negpitopi  14971  abssinper  14981  cos02pilt1  14986  relogeftb  15000  logbgcd1irraplemexp  15100  logbgcd1irrap  15102  lgsval  15120  lgsfvalg  15121  lgsfcl2  15122  lgsval2lem  15126  lgsmod  15142  lgsdilem  15143  lgsdir2lem4  15147  lgsdir2  15149  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  lgsquadlem1  15191  2sqlem5  15206  2sqlem6  15207  2sqlem7  15208  2sqlem9  15211  2sqlem10  15212  bj-findis  15471  pwle2  15489  pwf1oexmid  15490  pw1nct  15493  nnsf  15495  peano4nninf  15496  nninfall  15499  nninfsellemeq  15504  nninfsellemeqinf  15506  qdencn  15517  refeq  15518  trilpolemeq1  15530  trilpolemlt1  15531  trirec0  15534  nconstwlpolemgt0  15554  nconstwlpolem  15555  neapmkvlem  15557