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

Theorem adantld 467
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 461 . 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 369
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 371
This theorem is referenced by:  jaoa  510  dedlema  947  dedlemb  948  prlem1  955  2eu3  2384  unineq  3743  tz7.7  4899  ordsssuc2  4961  nnsuc  6690  poxp  6887  suppimacnv  6904  ressuppss  6911  imacosupp  6932  onnseq  7007  tz7.49  7102  oaass  7202  omordi  7207  nnmordi  7272  eroprf  7401  xpdom2  7604  inf3lem2  8037  trcl  8150  r1pwss  8193  cardaleph  8461  dfac2  8502  axcc4  8810  acncc  8811  zorn2lem7  8873  iundom2g  8906  cfpwsdom  8950  grothomex  9198  ltexprlem2  9406  1re  9586  00id  9745  mulge0  10061  nn0ge2m1nn  10852  uzindOLD  10946  xrlttr  11337  xmullem2  11448  snunioo  11637  fzen  11694  eluzgtdifelfzo  11837  ssfzo12bi  11866  modirr  12015  hash2pr  12470  hash3tr  12484  cshweqrep  12741  limsupbnd2  13257  climrlim2  13321  climuni  13326  mulcn2  13369  serf0  13454  cvgcmp  13581  smuval2  13982  qnumdencl  14122  infpnlem1  14278  ram0  14390  prmlem1  14442  prmlem2  14454  catass  14932  sscfn1  15038  subccocl  15063  funcco  15089  gsmsymgrfixlem1  16242  psgnran  16331  efgi  16528  efgi2  16534  cntzcmnss  16637  telgsumfzs  16804  dprddisj2  16872  dprddisj2OLD  16873  prmirredlem  18285  prmirredlemOLD  18288  psgnghm  18378  scmatghm  18797  cpmatacl  18979  pm2mpf1  19062  fvmptnn04if  19112  lmcls  19564  isfild  20089  flffbas  20226  cnpflf2  20231  divstgplem  20349  reperflem  21053  nmhmcn  21333  iscau2  21446  iscmet3lem2  21461  ivthlem2  21594  ovolmge0  21618  itg2seq  21879  limciun  22028  dveflem  22110  lhop1  22145  ftc1lem6  22172  mdegnn0cl  22201  aalioulem6  22462  pntlem3  23517  axlowdimlem16  23931  axcontlem12  23949  usgraedgprv  24040  usgra2wlkspthlem2  24284  usgrcyclnl2  24305  nvnencycllem  24307  wlkv0  24424  clwlkisclwwlklem2a4  24448  clwlkisclwwlklem1  24451  2spontn0vne  24551  usg2spthonot0  24553  iseupa  24629  frgra3vlem1  24664  ubthlem2  25451  shsvs  25905  mdsl2i  26905  mdsl2bi  26906  mdslmd1lem1  26908  atss  26929  chcv1  26938  chrelat2i  26948  atexch  26964  cdj3lem1  27017  bian1d  27030  disjxpin  27108  fpwrelmap  27216  nn0min  27267  sigaclci  27760  dya2iocuni  27882  subfacp1lem6  28257  ntrivcvg  28596  dfon2lem6  28785  dfrdg4  29165  altopth2  29181  cgrtriv  29217  cgrextend  29223  lineext  29291  btwnconn1  29316  colinbtwnle  29333  itg2addnc  29635  ftc1cnnc  29655  areacirclem1  29673  trer  29700  elicc3  29701  prnc  30056  ispridlc  30059  eldioph2b  30289  pell1234qrreccl  30383  islssfg2  30612  hbtlem2  30668  2reu3  31617  usgvincvad  31808  usgvincvadALT  31811  ztprmneprm  31877  pgrpgt2nabl  31901  snlindsntor  32022  sspwtrALT2  32580  bj-dfif5ALT  33107  bj-19.40b  33185  lcvexchlem4  33711  lcvexchlem5  33712  lkrss2N  33843  cvrnbtwn  33945  hlrelat2  34076  atle  34109  lvolex3N  34211  lplnnlelln  34216  llncvrlpln2  34230  lvolnlelln  34257  lvolnlelpln  34258  lplncvrlvol2  34288  snatpsubN  34423  linepsubN  34425  pmodlem2  34520  linepsubclN  34624  dihatexv  36012
  Copyright terms: Public domain W3C validator