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  8505  apirr  8935  mulge0  8949  lemul12a  9194  lediv2a  9227  creur  9291  nndiv  9347  zaddcllemneg  9687  peano5uzti  9758  supinfneg  10004  infsupneg  10005  divfnzn  10030  xrltso  10208  xpncan  10283  xltadd1  10288  xleaddadd  10299  elioc2  10348  elico2  10349  elicc2  10350  exfzdc  10669  zsupcllemstep  10672  infssuzex  10676  suprzubdc  10681  exbtwnzlemex  10694  rebtwn2z  10699  modqid  10799  modqcyc  10809  mulqaddmodid  10814  modqadd2mod  10824  addmodlteq  10848  frecuzrdgg  10866  nninfinf  10893  seq3val  10910  seqvalcd  10911  seq3clss  10921  iseqf1olemqcl  10949  iseqf1olemnab  10951  seq3f1olemp  10965  seq3f1o  10967  seqf1oglem1  10969  seqfeq4g  10981  fser0const  10985  ser3ge0  10986  exp3vallem  10990  qsqeqor  11100  nn0sqdc  11160  facndiv  11191  faclbnd  11193  bcval5  11215  hashen  11237  fihashdom  11257  hashunlem  11258  hashfacen  11298  zfz1isolemiso  11305  seq3coll  11308  ccatsymb  11384  ccatrn  11391  ccatw2s1p2  11428  swrdccatin1  11511  swrdccatin2  11515  swrdccat3b  11526  caucvgre  11761  resqrexlemlo  11793  cau3lem  11895  qdenre  11983  rexico  12002  fimaxre2  12008  2zinfmin  12025  xrmaxiflemcl  12027  xrmaxifle  12028  xrmaxiflemcom  12031  2clim  12083  cn1lem  12096  climsqz  12117  climsqz2  12118  climcau  12129  sumrbdclem  12160  summodclem2a  12164  fsum3  12170  fsumcl2lem  12181  fsumadd  12189  sumsnf  12192  fsum2dlemstep  12217  fisum0diag2  12230  fsummulc2  12231  mertenslemub  12317  mertenslemi1  12318  mertensabs  12320  ntrivcvgap  12331  prodrbdclem  12354  prodmodclem3  12358  prodmodclem2a  12359  prodmodc  12361  prod1dc  12369  prodsnf  12375  fprod2dlemstep  12405  efaddlem  12457  tanaddaplem  12521  zdvdsdc  12595  dvdseq  12631  dvdsext  12638  odd2np1  12656  sqoddm1div8z  12669  nno  12689  dfgcd3  12803  nninfctlemfo  12833  dvdslcm  12863  lcmneg  12868  lcmgcdlem  12871  ncoprmgcdne1b  12883  qredeq  12890  qredeu  12891  divgcdcoprm0  12895  exprmfct  12933  prmdvdsfz  12934  isprm5  12937  rpexp1i  12949  sqrt2irr  12957  nonsq  13003  sqrtrirr  13005  eulerthlemrprm  13027  eulerthlema  13028  phisum  13039  modprmn0modprm0  13055  pclemdc  13087  pcz  13131  pcmpt  13142  fldivp1  13147  pcfac  13149  expnprm  13152  oddprmdvds  13153  prmpwdvds  13154  infpnlem1  13158  1arith  13166  4sqlem2  13188  4sqlemafi  13194  4sqleminfi  13196  4sqexercise2  13198  4sqlemsdc  13199  ballotfilemsv  13302  ballotfilemsima  13308  ctinfom  13368  enctlem  13372  nninfdclemlt  13391  setsfun  13436  setsfun0  13437  setscom  13441  gzsumfzval  13760  mndissubm  13831  resmhm  13843  resmhm2  13844  mhmco  13846  gzsumwsubmcl  13850  gzsumwmhm  13852  dfgrp2  13881  isgrpinv  13908  mulgval  13974  mulgnnp1  13982  mulgz  14002  grpissubg  14046  resghm  14112  qusecsub  14184  gsumf1ofi  14209  isrng  14282  lmodfopne  14712  dflidl2rng  14867  mulgrhm2  14994  znidomb  15042  znunit  15043  issubassa2  15084  psrbaglesuppg  15106  psrbagfi  15108  tgdom  15222  ssrest  15332  cnfval  15344  cnpfval  15345  cnpval  15348  iscnp3  15353  ssidcn  15360  cnpnei  15369  cnntr  15375  cncnp  15380  cnptopresti  15388  tx1cn  15419  upxp  15422  imasnopn  15449  bdmet  15652  metcnp  15662  ivthinclemlr  15787  ivthinclemur  15789  ivthinc  15793  dvrecap  15863  dvmptfsum  15875  elply2  15885  plymullem1  15898  plycolemc  15908  plycjlemc  15910  dvply1  15915  pilem3  15934  relogeftb  16016  logbgcd1irr  16122  birthdaylem3  16146  mpodvdsmulf1o  16185  mersenne  16195  bposlem1  16209  bposlem3  16211  bposlem5  16213  lgslem4  16220  lgsval  16221  lgsfvalg  16222  lgsval2lem  16227  lgsmod  16243  lgsdir2lem4  16248  lgsdinn0  16265  lgsquad2lem2  16299  lgsquad3  16301  2lgslem1c  16307  2sqlem6  16337  2sqlem7  16338  isupgren  16434  wrdupgren  16435  isumgren  16444  wrdumgren  16445  isuspgren  16496  isusgren  16497  clwwlkext2edg  16761  clwwlknonex2  16778  depindlem3  16847  pw1map  17123  nnsf  17146  peano4nninf  17147  nninfalllem1  17149  nninfsellemqall  17156  nninfsellemeqinf  17157  nninffeq  17161  exmidsbthrlem  17165  isomninnlem  17177  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200