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

Theorem adantld 465
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 459 . 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 367
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 185  df-an 369
This theorem is referenced by:  jaoa  508  dedlema  952  dedlemb  953  prlem1  960  19.40b  1703  2eu3  2376  unineq  3745  tz7.7  4893  ordsssuc2  4955  nnsuc  6690  poxp  6885  suppimacnv  6902  ressuppss  6911  imacosupp  6932  onnseq  7007  tz7.49  7102  oaass  7202  omordi  7207  nnmordi  7272  eroprf  7401  xpdom2  7605  inf3lem2  8037  trcl  8150  r1pwss  8193  cardaleph  8461  dfac2  8502  axcc4  8810  acncc  8811  zorn2lem7  8873  iundom2g  8906  cfpwsdom  8950  grothomex  9196  ltexprlem2  9404  1re  9584  00id  9744  mulge0  10066  nn0ge2m1nn  10857  uzindOLD  10953  xrlttr  11349  xmullem2  11460  snunioo  11649  fzen  11706  eluzgtdifelfzo  11859  ssfzo12bi  11888  modirr  12039  hash2pr  12499  hash3tr  12513  cshweqrep  12780  limsupbnd2  13388  climrlim2  13452  climuni  13457  mulcn2  13500  serf0  13585  cvgcmp  13712  ntrivcvg  13788  smuval2  14216  qnumdencl  14356  infpnlem1  14512  ram0  14624  prmlem1  14677  prmlem2  14689  catass  15175  inveq  15262  sscfn1  15305  catsubcat  15327  subccocl  15333  funcco  15359  initoeu2  15494  funcestrcsetclem8  15615  funcsetcestrclem8  15630  gsmsymgrfixlem1  16651  psgnran  16739  efgi  16936  efgi2  16942  cntzcmnss  17048  telgsumfzs  17213  dprddisj2  17282  dprddisj2OLD  17283  prmirredlem  18705  psgnghm  18789  scmatghm  19202  cpmatacl  19384  pm2mpf1  19467  fvmptnn04if  19517  lmcls  19970  isfild  20525  flffbas  20662  cnpflf2  20667  qustgplem  20785  reperflem  21489  nmhmcn  21769  iscau2  21882  iscmet3lem2  21897  ivthlem2  22030  ovolmge0  22054  itg2seq  22315  limciun  22464  dveflem  22546  lhop1  22581  ftc1lem6  22608  mdegnn0cl  22637  aalioulem6  22899  pntlem3  23992  axlowdimlem16  24462  axcontlem12  24480  usgraedgprv  24578  usgra2wlkspthlem2  24822  usgrcyclnl2  24843  nvnencycllem  24845  wlkv0  24962  clwlkisclwwlklem2a4  24986  clwlkisclwwlklem1  24989  2spontn0vne  25089  usg2spthonot0  25091  iseupa  25167  frgra3vlem1  25202  ubthlem2  25985  shsvs  26439  mdsl2i  27439  mdsl2bi  27440  mdslmd1lem1  27442  atss  27463  chcv1  27472  chrelat2i  27482  atexch  27498  cdj3lem1  27551  bian1d  27564  disjxpin  27658  fpwrelmap  27787  nn0min  27845  sigaclci  28362  dya2iocuni  28491  omssubadd  28508  subfacp1lem6  28893  mthmblem  29204  dfon2lem6  29460  dfrdg4  29828  altopth2  29844  cgrtriv  29880  cgrextend  29886  lineext  29954  btwnconn1  29979  colinbtwnle  29996  itg2addnc  30309  ftc1cnnc  30329  areacirclem1  30347  trer  30374  elicc3  30375  prnc  30704  ispridlc  30707  eldioph2b  30935  pell1234qrreccl  31029  islssfg2  31256  hbtlem2  31314  lcmgcdlem  31453  lcmdvds  31455  2reu3  32432  usgvincvad  32776  usgvincvadALT  32779  mgmpropd  32835  rnghmsubcsetclem2  33038  funcrngcsetc  33060  rhmsubcsetclem2  33084  rhmsubcrngclem2  33090  funcringcsetc  33097  srhmsubc  33138  rhmsubclem4  33151  srhmsubcALTV  33157  rhmsubcALTVlem4  33170  ztprmneprm  33190  pgrpgt2nabl  33213  snlindsntor  33326  elbigo2  33427  sspwtrALT2  34023  lcvexchlem4  35159  lcvexchlem5  35160  lkrss2N  35291  cvrnbtwn  35393  hlrelat2  35524  atle  35557  lvolex3N  35659  lplnnlelln  35664  llncvrlpln2  35678  lvolnlelln  35705  lvolnlelpln  35706  lplncvrlvol2  35736  snatpsubN  35871  linepsubN  35873  pmodlem2  35968  linepsubclN  36072  dihatexv  37462
  Copyright terms: Public domain W3C validator