MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantld 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  1953  equveli  2028  2eu3  2322  unineq  3536  tz7.7  4550  ordsssuc2  4612  nnsuc  4804  poxp  6396  onnseq  6544  tz7.49  6640  oaass  6742  omordi  6747  nnmordi  6812  eroprf  6940  xpdom2  7141  inf3lem2  7519  trcl  7599  r1pwss  7645  cardaleph  7905  dfac2  7946  axcc4  8254  acncc  8255  zorn2lem7  8317  iundom2g  8350  cfpwsdom  8394  grothomex  8639  ltexprlem2  8849  1re  9025  00id  9175  mulge0  9479  uzindOLD  10298  xrlttr  10667  xmullem2  10778  snunioo  10957  fzen  11006  modirr  11215  hash2pr  11616  limsupbnd2  12206  climrlim2  12270  climuni  12275  mulcn2  12318  serf0  12403  cvgcmp  12524  smuval2  12923  qnumdencl  13060  infpnlem1  13207  ram0  13319  prmlem1  13359  prmlem2  13371  catass  13840  sscfn1  13946  subccocl  13971  funcco  13997  efgi  15280  efgi2  15286  dprddisj2  15526  prmirredlem  16698  lmcls  17290  isfild  17813  flffbas  17950  cnpflf2  17955  divstgplem  18073  reperflem  18722  nmhmcn  19001  iscau2  19103  iscmet3lem2  19118  ivthlem2  19218  ovolmge0  19242  itg2seq  19503  limciun  19650  dveflem  19732  lhop1  19767  ftc1lem6  19794  mdegnn0cl  19863  aalioulem6  20123  pntlem3  21172  usgraedgprv  21265  usgrcyclnl2  21478  nvnencycllem  21480  iseupa  21537  ubthlem2  22223  shsvs  22675  mdsl2i  23675  mdsl2bi  23676  mdslmd1lem1  23678  atss  23699  chcv1  23708  chrelat2i  23718  atexch  23734  cdj3lem1  23787  bian1d  23800  sigaclci  24313  dya2iocuni  24429  subfacp1lem6  24652  ntrivcvg  25006  dfon2lem6  25170  dfrdg4  25515  altopth2  25527  axlowdimlem16  25612  axcontlem12  25630  cgrtriv  25652  cgrextend  25658  lineext  25726  btwnconn1  25751  colinbtwnle  25768  itg2addnc  25961  ftc1cnnc  25981  areacirclem2  25984  trer  26012  elicc3  26013  prnc  26370  ispridlc  26373  eldioph2b  26514  pell1234qrreccl  26610  islssfg2  26840  hbtlem2  26999  psgnghm  27108  2reu3  27636  frgra3vlem1  27755  sspwtrALT2  28279  spimedNEW7  28850  equveliNEW7  28866  lcvexchlem4  29154  lcvexchlem5  29155  lkrss2N  29286  cvrnbtwn  29388  hlrelat2  29519  atle  29552  lvolex3N  29654  lplnnlelln  29659  llncvrlpln2  29673  lvolnlelln  29700  lvolnlelpln  29701  lplncvrlvol2  29731  snatpsubN  29866  linepsubN  29868  pmodlem2  29963  linepsubclN  30067  dihatexv  31455
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