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

Theorem adantld 455
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 449 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adantld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 31 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  jaoa  498  dedlema  922  dedlemb  923  prlem1  930  spimedOLD  1962  equveliOLD  2087  2eu3  2365  unineq  3593  tz7.7  4609  ordsssuc2  4672  nnsuc  4864  poxp  6460  onnseq  6608  tz7.49  6704  oaass  6806  omordi  6811  nnmordi  6876  eroprf  7004  xpdom2  7205  inf3lem2  7586  trcl  7666  r1pwss  7712  cardaleph  7972  dfac2  8013  axcc4  8321  acncc  8322  zorn2lem7  8384  iundom2g  8417  cfpwsdom  8461  grothomex  8706  ltexprlem2  8916  1re  9092  00id  9243  mulge0  9547  uzindOLD  10366  xrlttr  10735  xmullem2  10846  snunioo  11025  fzen  11074  modirr  11288  hash2pr  11689  limsupbnd2  12279  climrlim2  12343  climuni  12348  mulcn2  12391  serf0  12476  cvgcmp  12597  smuval2  12996  qnumdencl  13133  infpnlem1  13280  ram0  13392  prmlem1  13432  prmlem2  13444  catass  13913  sscfn1  14019  subccocl  14044  funcco  14070  efgi  15353  efgi2  15359  dprddisj2  15599  prmirredlem  16775  lmcls  17368  isfild  17892  flffbas  18029  cnpflf2  18034  divstgplem  18152  reperflem  18851  nmhmcn  19130  iscau2  19232  iscmet3lem2  19247  ivthlem2  19351  ovolmge0  19375  itg2seq  19636  limciun  19783  dveflem  19865  lhop1  19900  ftc1lem6  19927  mdegnn0cl  19996  aalioulem6  20256  pntlem3  21305  usgraedgprv  21398  usgrcyclnl2  21630  nvnencycllem  21632  iseupa  21689  ubthlem2  22375  shsvs  22827  mdsl2i  23827  mdsl2bi  23828  mdslmd1lem1  23830  atss  23851  chcv1  23860  chrelat2i  23870  atexch  23886  cdj3lem1  23939  bian1d  23952  disjxpin  24030  sigaclci  24517  dya2iocuni  24635  subfacp1lem6  24873  ntrivcvg  25227  dfon2lem6  25417  dfrdg4  25797  altopth2  25813  axlowdimlem16  25898  axcontlem12  25916  cgrtriv  25938  cgrextend  25944  lineext  26012  btwnconn1  26037  colinbtwnle  26054  itg2addnc  26261  ftc1cnnc  26281  areacirclem1  26294  trer  26321  elicc3  26322  prnc  26679  ispridlc  26682  eldioph2b  26823  pell1234qrreccl  26919  islssfg2  27148  hbtlem2  27307  psgnghm  27416  2reu3  27944  cshwssizelem2  28303  usgra2wlkspthlem2  28333  2spontn0vne  28407  usg2spthonot0  28409  frgra3vlem1  28452  sspwtrALT2  28998  spimedNEW7  29572  equveliNEW7  29590  lcvexchlem4  29897  lcvexchlem5  29898  lkrss2N  30029  cvrnbtwn  30131  hlrelat2  30262  atle  30295  lvolex3N  30397  lplnnlelln  30402  llncvrlpln2  30416  lvolnlelln  30443  lvolnlelpln  30444  lplncvrlvol2  30474  snatpsubN  30609  linepsubN  30611  pmodlem2  30706  linepsubclN  30810  dihatexv  32198
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 179  df-an 362
  Copyright terms: Public domain W3C validator