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  4587  en2lp  4615  foun  5558  f1oprg  5584  fcof1o  5876  foeqcnvco  5877  f1eqcocnv  5878  caovord3  6138  f1o2ndf1  6332  smores2  6398  frecrdg  6512  nnaordex  6632  xpdom2  6946  xpen  6962  mapen  6963  xpmapenlem  6966  nndomo  6981  phpm  6983  fidifsnen  6988  isinfinf  7015  finexdc  7020  fientri3  7033  fiintim  7049  xpfi  7050  f1dmvrnfibi  7067  sbthlemi8  7087  djudom  7216  omp1eomlem  7217  difinfsn  7223  ctmlemr  7231  ctssdccl  7234  nnnninfeq  7251  enomnilem  7261  finomni  7263  ismkvnex  7278  enmkvlem  7284  nninfwlpoimlemginf  7299  exmidfodomrlemrALT  7337  exmidontriim  7363  netap  7396  exmidapne  7402  acnccim  7414  dfplpq2  7497  recclnq  7535  subhalfnqq  7557  distrnq0  7602  prarloclem3step  7639  genpml  7660  genpmu  7661  addnqprl  7672  addnqpru  7673  appdivnq  7706  mulnqprl  7711  mulnqpru  7712  mullocpr  7714  ltexprlemfl  7752  ltexprlemfu  7754  ltmprr  7785  archpr  7786  cauappcvgprlemm  7788  caucvgprlemladdrl  7821  caucvgprprlemopl  7840  caucvgprprlemopu  7842  recexgt0sr  7916  mulgt0sr  7921  elrealeu  7972  axcaucvglemcau  8041  axcaucvglemres  8042  cnegex  8280  apirr  8708  mulge0  8722  lemul12a  8965  lediv2a  8998  creur  9062  nndiv  9107  zaddcllemneg  9441  peano5uzti  9511  supinfneg  9746  infsupneg  9747  divfnzn  9772  xrltso  9948  xpncan  10023  xltadd1  10028  xleaddadd  10039  elioc2  10088  elico2  10089  elicc2  10090  exfzdc  10401  zsupcllemstep  10404  infssuzex  10408  suprzubdc  10411  exbtwnzlemex  10424  rebtwn2z  10429  modqid  10526  modqcyc  10536  mulqaddmodid  10541  modqadd2mod  10551  addmodlteq  10575  frecuzrdgg  10593  nninfinf  10620  seq3val  10637  seqvalcd  10638  seq3clss  10648  iseqf1olemqcl  10676  iseqf1olemnab  10678  seq3f1olemp  10692  seq3f1o  10694  seqf1oglem1  10696  seqfeq4g  10708  fser0const  10712  ser3ge0  10713  exp3vallem  10717  qsqeqor  10827  facndiv  10916  faclbnd  10918  bcval5  10940  hashen  10961  fihashdom  10980  hashunlem  10981  hashfacen  11013  zfz1isolemiso  11016  seq3coll  11019  ccatsymb  11091  ccatrn  11098  ccatw2s1p2  11130  caucvgre  11377  resqrexlemlo  11409  cau3lem  11510  qdenre  11598  rexico  11617  fimaxre2  11623  2zinfmin  11639  xrmaxiflemcl  11641  xrmaxifle  11642  xrmaxiflemcom  11645  2clim  11697  cn1lem  11710  climsqz  11731  climsqz2  11732  climcau  11743  sumrbdclem  11773  summodclem2a  11777  fsum3  11783  fsumcl2lem  11794  fsumadd  11802  sumsnf  11805  fsum2dlemstep  11830  fisum0diag2  11843  fsummulc2  11844  mertenslemub  11930  mertenslemi1  11931  mertensabs  11933  ntrivcvgap  11944  prodrbdclem  11967  prodmodclem3  11971  prodmodclem2a  11972  prodmodc  11974  prod1dc  11982  prodsnf  11988  fprod2dlemstep  12018  efaddlem  12070  tanaddaplem  12134  zdvdsdc  12208  dvdseq  12244  dvdsext  12251  odd2np1  12269  sqoddm1div8z  12282  nno  12302  dfgcd3  12416  nninfctlemfo  12446  dvdslcm  12476  lcmneg  12481  lcmgcdlem  12484  ncoprmgcdne1b  12496  qredeq  12503  qredeu  12504  divgcdcoprm0  12508  exprmfct  12545  prmdvdsfz  12546  isprm5  12549  rpexp1i  12561  sqrt2irr  12569  nonsq  12614  eulerthlemrprm  12636  eulerthlema  12637  phisum  12648  modprmn0modprm0  12664  pclemdc  12696  pcz  12740  pcmpt  12751  fldivp1  12756  pcfac  12758  expnprm  12761  oddprmdvds  12762  prmpwdvds  12763  infpnlem1  12767  1arith  12775  4sqlem2  12797  4sqlemafi  12803  4sqleminfi  12805  4sqexercise2  12807  4sqlemsdc  12808  ctinfom  12884  enctlem  12888  nninfdclemlt  12907  setsfun  12952  setsfun0  12953  setscom  12957  gsumfzval  13308  mndissubm  13392  resmhm  13404  resmhm2  13405  mhmco  13407  gsumfzz  13412  gsumwsubmcl  13413  gsumwmhm  13415  dfgrp2  13444  isgrpinv  13471  mulgval  13543  mulgnnp1  13551  mulgz  13571  grpissubg  13615  resghm  13681  qusecsub  13752  isrng  13781  lmodfopne  14173  dflidl2rng  14328  gsumfzfsumlemm  14434  mulgrhm2  14457  znidomb  14505  znunit  14506  psrbaglesuppg  14519  psrbagfi  14520  tgdom  14629  ssrest  14739  cnfval  14751  cnpfval  14752  cnpval  14755  iscnp3  14760  ssidcn  14767  cnpnei  14776  cnntr  14782  cncnp  14787  cnptopresti  14795  tx1cn  14826  upxp  14829  imasnopn  14856  bdmet  15059  metcnp  15069  ivthinclemlr  15194  ivthinclemur  15196  ivthinc  15200  dvrecap  15270  dvmptfsum  15282  elply2  15292  plymullem1  15305  plycolemc  15315  plycjlemc  15317  dvply1  15322  pilem3  15340  relogeftb  15422  logbgcd1irr  15524  mpodvdsmulf1o  15547  mersenne  15554  lgslem4  15565  lgsval  15566  lgsfvalg  15567  lgsval2lem  15572  lgsmod  15588  lgsdir2lem4  15593  lgsdinn0  15610  lgsquad2lem2  15644  lgsquad3  15646  2lgslem1c  15652  2sqlem6  15682  2sqlem7  15683  isupgren  15776  wrdupgren  15777  isumgren  15786  wrdumgren  15787  2omap  16102  pw1map  16104  nnsf  16114  peano4nninf  16115  nninfalllem1  16117  nninfsellemqall  16124  nninfsellemeqinf  16125  nninffeq  16129  exmidsbthrlem  16133  isomninnlem  16141  iswomninnlem  16160  iswomni0  16162  ismkvnnlem  16163