MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantld Structured version   Unicode version

Theorem adantld 454
Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)
Hypothesis
Ref Expression
adantld.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
adantld  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)

Proof of Theorem adantld
StepHypRef Expression
1 simpr 448 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adantld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 30 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  jaoa  497  dedlema  921  dedlemb  922  prlem1  929  spimedOLD  1961  equveliOLD  2082  2eu3  2362  unineq  3583  tz7.7  4599  ordsssuc2  4662  nnsuc  4854  poxp  6450  onnseq  6598  tz7.49  6694  oaass  6796  omordi  6801  nnmordi  6866  eroprf  6994  xpdom2  7195  inf3lem2  7574  trcl  7654  r1pwss  7700  cardaleph  7960  dfac2  8001  axcc4  8309  acncc  8310  zorn2lem7  8372  iundom2g  8405  cfpwsdom  8449  grothomex  8694  ltexprlem2  8904  1re  9080  00id  9231  mulge0  9535  uzindOLD  10354  xrlttr  10723  xmullem2  10834  snunioo  11013  fzen  11062  modirr  11276  hash2pr  11677  limsupbnd2  12267  climrlim2  12331  climuni  12336  mulcn2  12379  serf0  12464  cvgcmp  12585  smuval2  12984  qnumdencl  13121  infpnlem1  13268  ram0  13380  prmlem1  13420  prmlem2  13432  catass  13901  sscfn1  14007  subccocl  14032  funcco  14058  efgi  15341  efgi2  15347  dprddisj2  15587  prmirredlem  16763  lmcls  17356  isfild  17880  flffbas  18017  cnpflf2  18022  divstgplem  18140  reperflem  18839  nmhmcn  19118  iscau2  19220  iscmet3lem2  19235  ivthlem2  19339  ovolmge0  19363  itg2seq  19624  limciun  19771  dveflem  19853  lhop1  19888  ftc1lem6  19915  mdegnn0cl  19984  aalioulem6  20244  pntlem3  21293  usgraedgprv  21386  usgrcyclnl2  21618  nvnencycllem  21620  iseupa  21677  ubthlem2  22363  shsvs  22815  mdsl2i  23815  mdsl2bi  23816  mdslmd1lem1  23818  atss  23839  chcv1  23848  chrelat2i  23858  atexch  23874  cdj3lem1  23927  bian1d  23940  disjxpin  24018  sigaclci  24505  dya2iocuni  24623  subfacp1lem6  24861  ntrivcvg  25215  dfon2lem6  25403  dfrdg4  25760  altopth2  25776  axlowdimlem16  25861  axcontlem12  25879  cgrtriv  25901  cgrextend  25907  lineext  25975  btwnconn1  26000  colinbtwnle  26017  itg2addnc  26222  ftc1cnnc  26242  areacirclem2  26245  trer  26273  elicc3  26274  prnc  26631  ispridlc  26634  eldioph2b  26775  pell1234qrreccl  26871  islssfg2  27101  hbtlem2  27260  psgnghm  27369  2reu3  27897  cshwssizelem2  28208  usgra2wlkspthlem2  28224  2spontn0vne  28271  usg2spthonot0  28273  frgra3vlem1  28291  sspwtrALT2  28837  spimedNEW7  29411  equveliNEW7  29429  lcvexchlem4  29736  lcvexchlem5  29737  lkrss2N  29868  cvrnbtwn  29970  hlrelat2  30101  atle  30134  lvolex3N  30236  lplnnlelln  30241  llncvrlpln2  30255  lvolnlelln  30282  lvolnlelpln  30283  lplncvrlvol2  30313  snatpsubN  30448  linepsubN  30450  pmodlem2  30545  linepsubclN  30649  dihatexv  32037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator