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

Theorem adantld 453
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 447 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adantld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 28 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  jaoa  496  dedlema  920  dedlemb  921  prlem1  928  spimed  1917  equveli  1928  2eu3  2225  unineq  3419  tz7.7  4418  ordsssuc2  4481  nnsuc  4673  poxp  6227  onnseq  6361  tz7.49  6457  oaass  6559  omordi  6564  nnmordi  6629  eroprf  6756  xpdom2  6957  inf3lem2  7330  trcl  7410  r1pwss  7456  cardaleph  7716  dfac2  7757  axcc4  8065  acncc  8066  zorn2lem7  8129  iundom2g  8162  cfpwsdom  8206  grothomex  8451  ltexprlem2  8661  1re  8837  00id  8987  mulge0  9291  uzindOLD  10106  xrlttr  10474  xmullem2  10585  snunioo  10762  fzen  10811  modirr  11009  limsupbnd2  11957  climrlim2  12021  climuni  12026  mulcn2  12069  serf0  12153  cvgcmp  12274  smuval2  12673  qnumdencl  12810  infpnlem1  12957  ram0  13069  prmlem1  13109  prmlem2  13121  catass  13588  sscfn1  13694  subccocl  13719  funcco  13745  efgi  15028  efgi2  15034  dprddisj2  15274  prmirredlem  16446  lmcls  17030  isfild  17553  flffbas  17690  cnpflf2  17695  divstgplem  17803  reperflem  18323  nmhmcn  18601  iscau2  18703  iscmet3lem2  18718  ivthlem2  18812  ovolmge0  18836  itg2seq  19097  limciun  19244  dveflem  19326  lhop1  19361  ftc1lem6  19388  mdegnn0cl  19457  aalioulem6  19717  pntlem3  20758  ubthlem2  21450  shsvs  21902  mdsl2i  22902  mdsl2bi  22903  mdslmd1lem1  22905  atss  22926  chcv1  22935  chrelat2i  22945  atexch  22961  cdj3lem1  23014  bian1d  23122  sigaclci  23493  subfacp1lem6  23716  iseupa  23881  dfon2lem6  24144  dfrdg4  24488  altopth2  24500  axlowdimlem16  24585  axcontlem12  24603  cgrtriv  24625  cgrextend  24631  lineext  24699  btwnconn1  24724  colinbtwnle  24741  areacirclem2  24925  injrec2  25119  ltrooo  25404  limptlimpr2lem2  25575  intvconlem1  25703  cmpassoh  25801  setiscat  25979  clscnc  26010  trer  26227  elicc3  26228  prnc  26692  ispridlc  26695  eldioph2b  26842  pell1234qrreccl  26939  islssfg2  27169  hbtlem2  27328  psgnghm  27437  2reu3  27966  usgraedgprv  28122  frgra3vlem1  28178  sspwtrALT2  28597  lcvexchlem4  29227  lcvexchlem5  29228  lkrss2N  29359  cvrnbtwn  29461  hlrelat2  29592  atle  29625  lvolex3N  29727  lplnnlelln  29732  llncvrlpln2  29746  lvolnlelln  29773  lvolnlelpln  29774  lplncvrlvol2  29804  snatpsubN  29939  linepsubN  29941  pmodlem2  30036  linepsubclN  30140  dihatexv  31528
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 177  df-an 360
  Copyright terms: Public domain W3C validator