Theorem ad2antlr 493

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad3antlr  497  simplr  533  simplrl  541  simplrr  542  ordtri2or2exmidlem  4673  en2lp  4701  foun  5658  f1oprg  5685  fcof1o  5995  foeqcnvco  5996  f1eqcocnv  5997  caovord3  6263  f1o2ndf1  6464  suppfnss  6497  suppssdc  6500  suppssfvg  6503  smores2  6565  frecrdg  6679  nnaordex  6801  xpdom2  7129  xpen  7145  mapen  7146  xpmapenlem  7149  nndomo  7165  phpm  7167  fidifsnen  7172  isinfinf  7201  fidcen  7203  finexdc  7207  elssdc  7209  fientri3  7222  fiintim  7238  xpfi  7239  f1dmvrnfibi  7258  sbthlemi8  7281  2omap  7318  2omapfi  7320  djudom  7433  omp1eomlem  7434  difinfsn  7440  ctmlemr  7448  ctssdccl  7451  nnnninfeq  7468  enomnilem  7478  finomni  7480  ismkvnex  7495  enmkvlem  7501  nninfwlpoimlemginf  7516  exmidfodomrlemrALT  7555  exmidontriim  7581  netap  7620  exmidapne  7626  acnccim  7638  dfplpq2  7721  recclnq  7759  subhalfnqq  7781  distrnq0  7826  prarloclem3step  7863  genpml  7884  genpmu  7885  addnqprl  7896  addnqpru  7897  appdivnq  7930  mulnqprl  7935  mulnqpru  7936  mullocpr  7938  ltexprlemfl  7976  ltexprlemfu  7978  ltmprr  8009  archpr  8010  cauappcvgprlemm  8012  caucvgprlemladdrl  8045  caucvgprprlemopl  8064  caucvgprprlemopu  8066  recexgt0sr  8140  mulgt0sr  8145  elrealeu  8196  axcaucvglemcau  8265  axcaucvglemres  8266  cnegex  8504  apirr  8933  mulge0  8947  lemul12a  9192  lediv2a  9225  creur  9289  nndiv  9345  zaddcllemneg  9683  peano5uzti  9754  supinfneg  9995  infsupneg  9996  divfnzn  10021  xrltso  10198  xpncan  10273  xltadd1  10278  xleaddadd  10289  elioc2  10338  elico2  10339  elicc2  10340  exfzdc  10659  zsupcllemstep  10662  infssuzex  10666  suprzubdc  10671  exbtwnzlemex  10684  rebtwn2z  10689  modqid  10786  modqcyc  10796  mulqaddmodid  10801  modqadd2mod  10811  addmodlteq  10835  frecuzrdgg  10853  nninfinf  10880  seq3val  10897  seqvalcd  10898  seq3clss  10908  iseqf1olemqcl  10936  iseqf1olemnab  10938  seq3f1olemp  10952  seq3f1o  10954  seqf1oglem1  10956  seqfeq4g  10968  fser0const  10972  ser3ge0  10973  exp3vallem  10977  qsqeqor  11087  facndiv  11177  faclbnd  11179  bcval5  11201  hashen  11223  fihashdom  11243  hashunlem  11244  hashfacen  11284  zfz1isolemiso  11291  seq3coll  11294  ccatsymb  11370  ccatrn  11377  ccatw2s1p2  11414  swrdccatin1  11497  swrdccatin2  11501  swrdccat3b  11512  caucvgre  11747  resqrexlemlo  11779  cau3lem  11880  qdenre  11968  rexico  11987  fimaxre2  11993  2zinfmin  12009  xrmaxiflemcl  12011  xrmaxifle  12012  xrmaxiflemcom  12015  2clim  12067  cn1lem  12080  climsqz  12101  climsqz2  12102  climcau  12113  sumrbdclem  12144  summodclem2a  12148  fsum3  12154  fsumcl2lem  12165  fsumadd  12173  sumsnf  12176  fsum2dlemstep  12201  fisum0diag2  12214  fsummulc2  12215  mertenslemub  12301  mertenslemi1  12302  mertensabs  12304  ntrivcvgap  12315  prodrbdclem  12338  prodmodclem3  12342  prodmodclem2a  12343  prodmodc  12345  prod1dc  12353  prodsnf  12359  fprod2dlemstep  12389  efaddlem  12441  tanaddaplem  12505  zdvdsdc  12579  dvdseq  12615  dvdsext  12622  odd2np1  12640  sqoddm1div8z  12653  nno  12673  dfgcd3  12787  nninfctlemfo  12817  dvdslcm  12847  lcmneg  12852  lcmgcdlem  12855  ncoprmgcdne1b  12867  qredeq  12874  qredeu  12875  divgcdcoprm0  12879  exprmfct  12916  prmdvdsfz  12917  isprm5  12920  rpexp1i  12932  sqrt2irr  12940  nonsq  12985  eulerthlemrprm  13007  eulerthlema  13008  phisum  13019  modprmn0modprm0  13035  pclemdc  13067  pcz  13111  pcmpt  13122  fldivp1  13127  pcfac  13129  expnprm  13132  oddprmdvds  13133  prmpwdvds  13134  infpnlem1  13138  1arith  13146  4sqlem2  13168  4sqlemafi  13174  4sqleminfi  13176  4sqexercise2  13178  4sqlemsdc  13179  ballotfilemsv  13253  ballotfilemsima  13259  ctinfom  13319  enctlem  13323  nninfdclemlt  13342  setsfun  13387  setsfun0  13388  setscom  13392  gzsumfzval  13711  mndissubm  13782  resmhm  13794  resmhm2  13795  mhmco  13797  gzsumwsubmcl  13801  gzsumwmhm  13803  dfgrp2  13832  isgrpinv  13859  mulgval  13925  mulgnnp1  13933  mulgz  13953  grpissubg  13997  resghm  14063  qusecsub  14135  gsumf1ofi  14160  isrng  14233  lmodfopne  14663  dflidl2rng  14818  mulgrhm2  14945  znidomb  14993  znunit  14994  issubassa2  15035  psrbaglesuppg  15057  psrbagfi  15059  tgdom  15173  ssrest  15283  cnfval  15295  cnpfval  15296  cnpval  15299  iscnp3  15304  ssidcn  15311  cnpnei  15320  cnntr  15326  cncnp  15331  cnptopresti  15339  tx1cn  15370  upxp  15373  imasnopn  15400  bdmet  15603  metcnp  15613  ivthinclemlr  15738  ivthinclemur  15740  ivthinc  15744  dvrecap  15814  dvmptfsum  15826  elply2  15836  plymullem1  15849  plycolemc  15859  plycjlemc  15861  dvply1  15866  pilem3  15884  relogeftb  15966  logbgcd1irr  16069  birthdaylem3  16089  mpodvdsmulf1o  16104  mersenne  16111  lgslem4  16122  lgsval  16123  lgsfvalg  16124  lgsval2lem  16129  lgsmod  16145  lgsdir2lem4  16150  lgsdinn0  16167  lgsquad2lem2  16201  lgsquad3  16203  2lgslem1c  16209  2sqlem6  16239  2sqlem7  16240  isupgren  16336  wrdupgren  16337  isumgren  16346  wrdumgren  16347  isuspgren  16398  isusgren  16399  clwwlkext2edg  16663  clwwlknonex2  16680  depindlem3  16749  pw1map  17025  nnsf  17048  peano4nninf  17049  nninfalllem1  17051  nninfsellemqall  17058  nninfsellemeqinf  17059  nninffeq  17063  exmidsbthrlem  17067  isomninnlem  17079  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102