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

Theorem adantld 474
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 468 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adantld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 32 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  jaoa  519  dedlema  970  dedlemb  971  prlem1  974  19.40bOLD  1759  2eu3  2404  unineq  3684  tz7.7  5456  ordsssuc2  5518  nnsuc  6728  poxp  6927  suppimacnv  6944  ressuppss  6953  imacosupp  6974  onnseq  7081  tz7.49  7180  oaass  7280  omordi  7285  nnmordi  7350  eroprf  7479  xpdom2  7685  inf3lem2  8152  trcl  8230  r1pwss  8273  cardaleph  8538  dfac2  8579  axcc4  8887  acncc  8888  zorn2lem7  8950  iundom2g  8983  cfpwsdom  9027  grothomex  9272  ltexprlem2  9480  1re  9660  00id  9826  mulge0  10153  nn0ge2m1nn  10958  xrlttr  11462  xmullem2  11576  snunioo  11784  fzen  11842  eluzgtdifelfzo  12005  ssfzo12bi  12035  modirr  12194  hash2pr  12671  hash3tr  12688  cshf1  12966  cshweqrep  12977  limsupbnd2  13623  limsupbnd2OLD  13624  climrlim2  13688  climuni  13693  mulcn2  13736  serf0  13824  cvgcmp  13953  ntrivcvg  14030  smuval2  14535  lcmgcdlem  14650  lcmdvds  14652  lcmf  14685  qnumdencl  14767  infpnlem1  14933  ram0  15059  prmgaplem6  15105  prmgaplem7  15106  prmlem1  15157  prmlem2  15169  catass  15670  inveq  15757  sscfn1  15800  catsubcat  15822  subccocl  15828  funcco  15854  initoeu2  15989  funcestrcsetclem8  16110  funcsetcestrclem8  16125  gsmsymgrfixlem1  17146  psgnran  17234  efgi  17447  efgi2  17453  cntzcmnss  17559  telgsumfzs  17697  dprddisj2  17750  prmirredlem  19141  psgnghm  19225  scmatghm  19635  cpmatacl  19817  pm2mpf1  19900  fvmptnn04if  19950  lmcls  20395  isfild  20951  flffbas  21088  cnpflf2  21093  qustgplem  21213  reperflem  21914  nmhmcn  22212  iscau2  22325  iscmet3lem2  22340  ivthlem2  22481  ovolmge0  22508  itg2seq  22779  limciun  22928  dveflem  23010  lhop1  23045  ftc1lem6  23072  mdegnn0cl  23099  aalioulem6  23372  pntlem3  24526  axlowdimlem16  25066  axcontlem12  25084  usgraedgprv  25182  usgra2wlkspthlem2  25427  usgrcyclnl2  25448  nvnencycllem  25450  wlkv0  25567  clwlkisclwwlklem2a4  25591  clwlkisclwwlklem1  25594  2spontn0vne  25694  usg2spthonot0  25696  iseupa  25772  frgra3vlem1  25807  ubthlem2  26594  shsvs  27057  mdsl2i  28056  mdsl2bi  28057  mdslmd1lem1  28059  atss  28080  chcv1  28089  chrelat2i  28099  atexch  28115  cdj3lem1  28168  bian1d  28181  disjxpin  28275  fpwrelmap  28393  nn0min  28459  sigaclci  29028  dya2iocuni  29178  omssubadd  29201  omssubaddOLD  29205  subfacp1lem6  29980  mthmblem  30290  dfon2lem6  30505  dfrdg4  30789  altopth2  30804  cgrtriv  30840  cgrextend  30846  lineext  30914  btwnconn1  30939  colinbtwnle  30956  trer  31043  elicc3  31044  poimirlem27  32031  poimirlem29  32033  poimir  32037  itg2addnc  32060  ftc1cnnc  32080  areacirclem1  32096  prnc  32364  ispridlc  32367  lcvexchlem4  32674  lcvexchlem5  32675  lkrss2N  32806  cvrnbtwn  32908  hlrelat2  33039  atle  33072  lvolex3N  33174  lplnnlelln  33179  llncvrlpln2  33193  lvolnlelln  33220  lvolnlelpln  33221  lplncvrlvol2  33251  snatpsubN  33386  linepsubN  33388  pmodlem2  33483  linepsubclN  33587  dihatexv  34977  eldioph2b  35676  pell1234qrreccl  35771  islssfg2  36000  hbtlem2  36054  clss2lem  36289  sspwtrALT2  37282  2reu3  38754  iccpartres  38877  iccpartiltu  38881  icceuelpart  38895  bgoldbwt  39023  bgoldbst  39024  nnsum4primesoddALTV  39037  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  bgoldbtbndlem2  39046  fpropnf1  39182  umgrislfupgrlem  39367  uhgr2edg  39453  ushgredgedga  39470  ushgredgedgaloop  39472  nbuhgr2vtx1edgb  39584  edgnbusgreu  39605  usgredgsscusgredg  39685  wlkOnwlk1l  39861  1wlkdlem2  39883  pthdivtx  39922  upgrwlkdvdelem  39928  spthonepeq-av  39944  pthdlem1  39952  crctcshlem4  39998  uhgr3cyclexlem  40095  eucrctshift  40155  usgvincvad  40224  usgvincvadALT  40227  mgmpropd  40283  rnghmsubcsetclem2  40486  funcrngcsetc  40508  rhmsubcsetclem2  40532  rhmsubcrngclem2  40538  funcringcsetc  40545  srhmsubc  40586  rhmsubclem4  40599  srhmsubcALTV  40605  rhmsubcALTVlem4  40618  ztprmneprm  40636  pgrpgt2nabl  40659  snlindsntor  40772  elbigo2  40871
  Copyright terms: Public domain W3C validator