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  529  simplrl  537  simplrr  538  ordtri2or2exmidlem  4653  en2lp  4681  foun  5638  f1oprg  5665  fcof1o  5968  foeqcnvco  5969  f1eqcocnv  5970  caovord3  6236  f1o2ndf1  6437  suppfnss  6470  suppssdc  6473  suppssfvg  6476  smores2  6538  frecrdg  6652  nnaordex  6774  xpdom2  7095  xpen  7111  mapen  7112  xpmapenlem  7115  nndomo  7131  phpm  7133  fidifsnen  7138  isinfinf  7167  fidcen  7169  finexdc  7173  elssdc  7175  fientri3  7188  fiintim  7204  xpfi  7205  f1dmvrnfibi  7224  sbthlemi8  7247  2omap  7282  2omapfi  7284  djudom  7397  omp1eomlem  7398  difinfsn  7404  ctmlemr  7412  ctssdccl  7415  nnnninfeq  7432  enomnilem  7442  finomni  7444  ismkvnex  7459  enmkvlem  7465  nninfwlpoimlemginf  7480  exmidfodomrlemrALT  7519  exmidontriim  7545  netap  7584  exmidapne  7590  acnccim  7602  dfplpq2  7685  recclnq  7723  subhalfnqq  7745  distrnq0  7790  prarloclem3step  7827  genpml  7848  genpmu  7849  addnqprl  7860  addnqpru  7861  appdivnq  7894  mulnqprl  7899  mulnqpru  7900  mullocpr  7902  ltexprlemfl  7940  ltexprlemfu  7942  ltmprr  7973  archpr  7974  cauappcvgprlemm  7976  caucvgprlemladdrl  8009  caucvgprprlemopl  8028  caucvgprprlemopu  8030  recexgt0sr  8104  mulgt0sr  8109  elrealeu  8160  axcaucvglemcau  8229  axcaucvglemres  8230  cnegex  8467  apirr  8896  mulge0  8910  lemul12a  9153  lediv2a  9186  creur  9250  nndiv  9295  zaddcllemneg  9633  peano5uzti  9704  supinfneg  9945  infsupneg  9946  divfnzn  9971  xrltso  10148  xpncan  10223  xltadd1  10228  xleaddadd  10239  elioc2  10288  elico2  10289  elicc2  10290  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  suprzubdc  10620  exbtwnzlemex  10633  rebtwn2z  10638  modqid  10735  modqcyc  10745  mulqaddmodid  10750  modqadd2mod  10760  addmodlteq  10784  frecuzrdgg  10802  nninfinf  10829  seq3val  10846  seqvalcd  10847  seq3clss  10857  iseqf1olemqcl  10885  iseqf1olemnab  10887  seq3f1olemp  10901  seq3f1o  10903  seqf1oglem1  10905  seqfeq4g  10917  fser0const  10921  ser3ge0  10922  exp3vallem  10926  qsqeqor  11036  facndiv  11126  faclbnd  11128  bcval5  11150  hashen  11172  fihashdom  11192  hashunlem  11193  hashfacen  11233  zfz1isolemiso  11236  seq3coll  11239  ccatsymb  11315  ccatrn  11322  ccatw2s1p2  11359  swrdccatin1  11442  swrdccatin2  11446  swrdccat3b  11457  caucvgre  11691  resqrexlemlo  11723  cau3lem  11824  qdenre  11912  rexico  11931  fimaxre2  11937  2zinfmin  11953  xrmaxiflemcl  11955  xrmaxifle  11956  xrmaxiflemcom  11959  2clim  12011  cn1lem  12024  climsqz  12045  climsqz2  12046  climcau  12057  sumrbdclem  12088  summodclem2a  12092  fsum3  12098  fsumcl2lem  12109  fsumadd  12117  sumsnf  12120  fsum2dlemstep  12145  fisum0diag2  12158  fsummulc2  12159  mertenslemub  12245  mertenslemi1  12246  mertensabs  12248  ntrivcvgap  12259  prodrbdclem  12282  prodmodclem3  12286  prodmodclem2a  12287  prodmodc  12289  prod1dc  12297  prodsnf  12303  fprod2dlemstep  12333  efaddlem  12385  tanaddaplem  12449  zdvdsdc  12523  dvdseq  12559  dvdsext  12566  odd2np1  12584  sqoddm1div8z  12597  nno  12617  dfgcd3  12731  nninfctlemfo  12761  dvdslcm  12791  lcmneg  12796  lcmgcdlem  12799  ncoprmgcdne1b  12811  qredeq  12818  qredeu  12819  divgcdcoprm0  12823  exprmfct  12860  prmdvdsfz  12861  isprm5  12864  rpexp1i  12876  sqrt2irr  12884  nonsq  12929  eulerthlemrprm  12951  eulerthlema  12952  phisum  12963  modprmn0modprm0  12979  pclemdc  13011  pcz  13055  pcmpt  13066  fldivp1  13071  pcfac  13073  expnprm  13076  oddprmdvds  13077  prmpwdvds  13078  infpnlem1  13082  1arith  13090  4sqlem2  13112  4sqlemafi  13118  4sqleminfi  13120  4sqexercise2  13122  4sqlemsdc  13123  ballotfilemsv  13197  ballotfilemsima  13203  ctinfom  13263  enctlem  13267  nninfdclemlt  13286  setsfun  13331  setsfun0  13332  setscom  13336  gsumfzval  13654  mndissubm  13730  resmhm  13742  resmhm2  13743  mhmco  13745  gsumfzz  13750  gsumwsubmcl  13751  gsumwmhm  13753  dfgrp2  13782  isgrpinv  13809  mulgval  13875  mulgnnp1  13883  mulgz  13903  grpissubg  13947  resghm  14013  qusecsub  14084  isrng  14173  lmodfopne  14600  dflidl2rng  14755  gsumfzfsumlemm  14861  mulgrhm2  14884  znidomb  14932  znunit  14933  psrbaglesuppg  14947  psrbagfi  14949  tgdom  15063  ssrest  15173  cnfval  15185  cnpfval  15186  cnpval  15189  iscnp3  15194  ssidcn  15201  cnpnei  15210  cnntr  15216  cncnp  15221  cnptopresti  15229  tx1cn  15260  upxp  15263  imasnopn  15290  bdmet  15493  metcnp  15503  ivthinclemlr  15628  ivthinclemur  15630  ivthinc  15634  dvrecap  15704  dvmptfsum  15716  elply2  15726  plymullem1  15739  plycolemc  15749  plycjlemc  15751  dvply1  15756  pilem3  15774  relogeftb  15856  logbgcd1irr  15958  mpodvdsmulf1o  15984  mersenne  15991  lgslem4  16002  lgsval  16003  lgsfvalg  16004  lgsval2lem  16009  lgsmod  16025  lgsdir2lem4  16030  lgsdinn0  16047  lgsquad2lem2  16081  lgsquad3  16083  2lgslem1c  16089  2sqlem6  16119  2sqlem7  16120  isupgren  16216  wrdupgren  16217  isumgren  16226  wrdumgren  16227  isuspgren  16278  isusgren  16279  clwwlkext2edg  16543  clwwlknonex2  16560  depindlem3  16629  pw1map  16895  nnsf  16909  peano4nninf  16910  nninfalllem1  16912  nninfsellemqall  16919  nninfsellemeqinf  16920  nninffeq  16924  exmidsbthrlem  16928  isomninnlem  16940  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963