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  1930  equveli  1941  2eu3  2238  unineq  3432  tz7.7  4434  ordsssuc2  4497  nnsuc  4689  poxp  6243  onnseq  6377  tz7.49  6473  oaass  6575  omordi  6580  nnmordi  6645  eroprf  6772  xpdom2  6973  inf3lem2  7346  trcl  7426  r1pwss  7472  cardaleph  7732  dfac2  7773  axcc4  8081  acncc  8082  zorn2lem7  8145  iundom2g  8178  cfpwsdom  8222  grothomex  8467  ltexprlem2  8677  1re  8853  00id  9003  mulge0  9307  uzindOLD  10122  xrlttr  10490  xmullem2  10601  snunioo  10778  fzen  10827  modirr  11025  limsupbnd2  11973  climrlim2  12037  climuni  12042  mulcn2  12085  serf0  12169  cvgcmp  12290  smuval2  12689  qnumdencl  12826  infpnlem1  12973  ram0  13085  prmlem1  13125  prmlem2  13137  catass  13604  sscfn1  13710  subccocl  13735  funcco  13761  efgi  15044  efgi2  15050  dprddisj2  15290  prmirredlem  16462  lmcls  17046  isfild  17569  flffbas  17706  cnpflf2  17711  divstgplem  17819  reperflem  18339  nmhmcn  18617  iscau2  18719  iscmet3lem2  18734  ivthlem2  18828  ovolmge0  18852  itg2seq  19113  limciun  19260  dveflem  19342  lhop1  19377  ftc1lem6  19404  mdegnn0cl  19473  aalioulem6  19733  pntlem3  20774  ubthlem2  21466  shsvs  21918  mdsl2i  22918  mdsl2bi  22919  mdslmd1lem1  22921  atss  22942  chcv1  22951  chrelat2i  22961  atexch  22977  cdj3lem1  23030  bian1d  23138  sigaclci  23508  subfacp1lem6  23731  iseupa  23896  dfon2lem6  24215  dfrdg4  24560  altopth2  24572  axlowdimlem16  24657  axcontlem12  24675  cgrtriv  24697  cgrextend  24703  lineext  24771  btwnconn1  24796  colinbtwnle  24813  itg2addnc  25005  ftc1cnnc  25025  areacirclem2  25028  injrec2  25222  ltrooo  25507  limptlimpr2lem2  25678  intvconlem1  25806  cmpassoh  25904  setiscat  26082  clscnc  26113  trer  26330  elicc3  26331  prnc  26795  ispridlc  26798  eldioph2b  26945  pell1234qrreccl  27042  islssfg2  27272  hbtlem2  27431  psgnghm  27540  2reu3  28069  usgraedgprv  28256  usgrcyclnl2  28387  nvnencycllem  28389  frgra3vlem1  28424  sspwtrALT2  28913  spimedNEW7  29487  equveliNEW7  29503  lcvexchlem4  29849  lcvexchlem5  29850  lkrss2N  29981  cvrnbtwn  30083  hlrelat2  30214  atle  30247  lvolex3N  30349  lplnnlelln  30354  llncvrlpln2  30368  lvolnlelln  30395  lvolnlelpln  30396  lplncvrlvol2  30426  snatpsubN  30561  linepsubN  30563  pmodlem2  30658  linepsubclN  30762  dihatexv  32150
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