Theorem ad2antlr 489

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
ad2antlr	|- ( ( ( ch /\ ph ) /\ th ) -> ps )

Proof of Theorem ad2antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantll 476	1 |- ( ( ( ch /\ ph ) /\ 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:  ad3antlr  493  simplr  528  simplrl  535  simplrr  536  ordtri2or2exmidlem  4527  en2lp  4555  foun  5482  f1oprg  5507  fcof1o  5792  foeqcnvco  5793  f1eqcocnv  5794  caovord3  6050  f1o2ndf1  6231  smores2  6297  frecrdg  6411  nnaordex  6531  xpdom2  6833  xpen  6847  mapen  6848  xpmapenlem  6851  nndomo  6866  phpm  6867  fidifsnen  6872  isinfinf  6899  finexdc  6904  fientri3  6916  fiintim  6930  xpfi  6931  f1dmvrnfibi  6945  sbthlemi8  6965  djudom  7094  omp1eomlem  7095  difinfsn  7101  ctmlemr  7109  ctssdccl  7112  nnnninfeq  7128  enomnilem  7138  finomni  7140  ismkvnex  7155  enmkvlem  7161  nninfwlpoimlemginf  7176  exmidfodomrlemrALT  7204  exmidontriim  7226  netap  7255  exmidapne  7261  dfplpq2  7355  recclnq  7393  subhalfnqq  7415  distrnq0  7460  prarloclem3step  7497  genpml  7518  genpmu  7519  addnqprl  7530  addnqpru  7531  appdivnq  7564  mulnqprl  7569  mulnqpru  7570  mullocpr  7572  ltexprlemfl  7610  ltexprlemfu  7612  ltmprr  7643  archpr  7644  cauappcvgprlemm  7646  caucvgprlemladdrl  7679  caucvgprprlemopl  7698  caucvgprprlemopu  7700  recexgt0sr  7774  mulgt0sr  7779  elrealeu  7830  axcaucvglemcau  7899  axcaucvglemres  7900  cnegex  8137  apirr  8564  mulge0  8578  lemul12a  8821  lediv2a  8854  creur  8918  nndiv  8962  zaddcllemneg  9294  peano5uzti  9363  supinfneg  9597  infsupneg  9598  divfnzn  9623  xrltso  9798  xpncan  9873  xltadd1  9878  xleaddadd  9889  elioc2  9938  elico2  9939  elicc2  9940  exfzdc  10242  exbtwnzlemex  10252  rebtwn2z  10257  modqid  10351  modqcyc  10361  mulqaddmodid  10366  modqadd2mod  10376  addmodlteq  10400  frecuzrdgg  10418  seq3val  10460  seqvalcd  10461  seq3clss  10469  iseqf1olemqcl  10488  iseqf1olemnab  10490  seq3f1olemp  10504  seq3f1o  10506  fser0const  10518  ser3ge0  10519  exp3vallem  10523  qsqeqor  10633  facndiv  10721  faclbnd  10723  bcval5  10745  hashen  10766  fihashdom  10785  hashunlem  10786  hashfacen  10818  zfz1isolemiso  10821  seq3coll  10824  caucvgre  10992  resqrexlemlo  11024  cau3lem  11125  qdenre  11213  rexico  11232  fimaxre2  11237  2zinfmin  11253  xrmaxiflemcl  11255  xrmaxifle  11256  xrmaxiflemcom  11259  2clim  11311  cn1lem  11324  climsqz  11345  climsqz2  11346  climcau  11357  sumrbdclem  11387  summodclem2a  11391  fsum3  11397  fsumcl2lem  11408  fsumadd  11416  sumsnf  11419  fsum2dlemstep  11444  fisum0diag2  11457  fsummulc2  11458  mertenslemub  11544  mertenslemi1  11545  mertensabs  11547  ntrivcvgap  11558  prodrbdclem  11581  prodmodclem3  11585  prodmodclem2a  11586  prodmodc  11588  prod1dc  11596  prodsnf  11602  fprod2dlemstep  11632  efaddlem  11684  tanaddaplem  11748  zdvdsdc  11821  dvdseq  11856  dvdsext  11863  odd2np1  11880  sqoddm1div8z  11893  nno  11913  zsupcllemstep  11948  infssuzex  11952  suprzubdc  11955  dfgcd3  12013  dvdslcm  12071  lcmneg  12076  lcmgcdlem  12079  ncoprmgcdne1b  12091  qredeq  12098  qredeu  12099  divgcdcoprm0  12103  exprmfct  12140  prmdvdsfz  12141  isprm5  12144  rpexp1i  12156  sqrt2irr  12164  nonsq  12209  eulerthlemrprm  12231  eulerthlema  12232  phisum  12242  modprmn0modprm0  12258  pclemdc  12290  pcz  12333  pcmpt  12343  fldivp1  12348  pcfac  12350  expnprm  12353  oddprmdvds  12354  prmpwdvds  12355  infpnlem1  12359  1arith  12367  4sqlem2  12389  ctinfom  12431  enctlem  12435  nninfdclemlt  12454  setsfun  12499  setsfun0  12500  setscom  12504  mndissubm  12871  mhmco  12879  dfgrp2  12907  isgrpinv  12931  mulgval  12991  mulgnnp1  12996  mulgz  13016  grpissubg  13059  lmodfopne  13421  tgdom  13611  ssrest  13721  cnfval  13733  cnpfval  13734  cnpval  13737  iscnp3  13742  ssidcn  13749  cnpnei  13758  cnntr  13764  cncnp  13769  cnptopresti  13777  tx1cn  13808  upxp  13811  imasnopn  13838  bdmet  14041  metcnp  14051  ivthinclemlr  14154  ivthinclemur  14156  ivthinc  14160  dvrecap  14216  pilem3  14243  relogeftb  14325  logbgcd1irr  14424  lgslem4  14443  lgsval  14444  lgsfvalg  14445  lgsval2lem  14450  lgsmod  14466  lgsdir2lem4  14471  lgsdinn0  14488  2sqlem6  14506  2sqlem7  14507  nnsf  14793  peano4nninf  14794  nninfalllem1  14796  nninfsellemqall  14803  nninfsellemeqinf  14804  nninffeq  14808  exmidsbthrlem  14809  isomninnlem  14817  iswomninnlem  14836  iswomni0  14838  ismkvnnlem  14839