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

Theorem adantld 469
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 463 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adantld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 33 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  jaoa  513  dedlema  964  dedlemb  965  prlem1  972  19.40bOLD  1750  2eu3  2383  unineq  3692  tz7.7  5448  ordsssuc2  5510  nnsuc  6706  poxp  6905  suppimacnv  6922  ressuppss  6931  imacosupp  6952  onnseq  7060  tz7.49  7159  oaass  7259  omordi  7264  nnmordi  7329  eroprf  7458  xpdom2  7664  inf3lem2  8131  trcl  8209  r1pwss  8252  cardaleph  8517  dfac2  8558  axcc4  8866  acncc  8867  zorn2lem7  8929  iundom2g  8962  cfpwsdom  9006  grothomex  9251  ltexprlem2  9459  1re  9639  00id  9805  mulge0  10129  nn0ge2m1nn  10931  xrlttr  11436  xmullem2  11548  snunioo  11755  fzen  11813  eluzgtdifelfzo  11973  ssfzo12bi  12003  modirr  12157  hash2pr  12627  hash3tr  12644  cshweqrep  12915  limsupbnd2  13539  limsupbnd2OLD  13540  climrlim2  13604  climuni  13609  mulcn2  13652  serf0  13740  cvgcmp  13869  ntrivcvg  13946  smuval2  14449  lcmgcdlem  14564  lcmdvds  14566  lcmf  14599  qnumdencl  14681  infpnlem1  14847  ram0  14973  prmgaplem6  15019  prmgaplem7  15020  prmlem1  15072  prmlem2  15084  catass  15585  inveq  15672  sscfn1  15715  catsubcat  15737  subccocl  15743  funcco  15769  initoeu2  15904  funcestrcsetclem8  16025  funcsetcestrclem8  16040  gsmsymgrfixlem1  17061  psgnran  17149  efgi  17362  efgi2  17368  cntzcmnss  17474  telgsumfzs  17612  dprddisj2  17665  prmirredlem  19057  psgnghm  19141  scmatghm  19551  cpmatacl  19733  pm2mpf1  19816  fvmptnn04if  19866  lmcls  20311  isfild  20866  flffbas  21003  cnpflf2  21008  qustgplem  21128  reperflem  21829  nmhmcn  22127  iscau2  22240  iscmet3lem2  22255  ivthlem2  22396  ovolmge0  22423  itg2seq  22693  limciun  22842  dveflem  22924  lhop1  22959  ftc1lem6  22986  mdegnn0cl  23013  aalioulem6  23286  pntlem3  24440  axlowdimlem16  24980  axcontlem12  24998  usgraedgprv  25096  usgra2wlkspthlem2  25341  usgrcyclnl2  25362  nvnencycllem  25364  wlkv0  25481  clwlkisclwwlklem2a4  25505  clwlkisclwwlklem1  25508  2spontn0vne  25608  usg2spthonot0  25610  iseupa  25686  frgra3vlem1  25721  ubthlem2  26506  shsvs  26969  mdsl2i  27968  mdsl2bi  27969  mdslmd1lem1  27971  atss  27992  chcv1  28001  chrelat2i  28011  atexch  28027  cdj3lem1  28080  bian1d  28093  disjxpin  28191  fpwrelmap  28311  nn0min  28377  sigaclci  28947  dya2iocuni  29098  omssubadd  29121  omssubaddOLD  29125  subfacp1lem6  29901  mthmblem  30211  dfon2lem6  30427  dfrdg4  30711  altopth2  30726  cgrtriv  30762  cgrextend  30768  lineext  30836  btwnconn1  30861  colinbtwnle  30878  trer  30965  elicc3  30966  poimirlem27  31960  poimirlem29  31962  poimir  31966  itg2addnc  31989  ftc1cnnc  32009  areacirclem1  32025  prnc  32293  ispridlc  32296  lcvexchlem4  32597  lcvexchlem5  32598  lkrss2N  32729  cvrnbtwn  32831  hlrelat2  32962  atle  32995  lvolex3N  33097  lplnnlelln  33102  llncvrlpln2  33116  lvolnlelln  33143  lvolnlelpln  33144  lplncvrlvol2  33174  snatpsubN  33309  linepsubN  33311  pmodlem2  33406  linepsubclN  33510  dihatexv  34900  eldioph2b  35599  pell1234qrreccl  35694  islssfg2  35923  hbtlem2  35977  clss2lem  36212  sspwtrALT2  37213  2reu3  38603  iccpartres  38726  iccpartiltu  38730  icceuelpart  38744  bgoldbwt  38872  bgoldbst  38873  nnsum4primesoddALTV  38886  nnsum4primeseven  38889  nnsum4primesevenALTV  38890  bgoldbtbndlem2  38895  usgr2edg  39277  ushgredgedga  39292  ushgredgedgaloop  39294  nbuhgr2vtx1edgb  39403  edgnbusgreu  39424  usgredgsscusgredg  39503  wlk1wlk  39632  usgvincvad  39703  usgvincvadALT  39706  mgmpropd  39762  rnghmsubcsetclem2  39965  funcrngcsetc  39987  rhmsubcsetclem2  40011  rhmsubcrngclem2  40017  funcringcsetc  40024  srhmsubc  40065  rhmsubclem4  40078  srhmsubcALTV  40084  rhmsubcALTVlem4  40097  ztprmneprm  40115  pgrpgt2nabl  40138  snlindsntor  40251  elbigo2  40350
  Copyright terms: Public domain W3C validator