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

Theorem syl7 63
Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
Hypotheses
Ref Expression
syl7.1  |-  ( ph  ->  ps )
syl7.2  |-  ( ch 
->  ( th  ->  ( ps  ->  ta ) ) )
Assertion
Ref Expression
syl7  |-  ( ch 
->  ( th  ->  ( ph  ->  ta ) ) )

Proof of Theorem syl7
StepHypRef Expression
1 syl7.1 . . 3  |-  ( ph  ->  ps )
21a1i 10 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
3 syl7.2 . 2  |-  ( ch 
->  ( th  ->  ( ps  ->  ta ) ) )
42, 3syl5d 62 1  |-  ( ch 
->  ( th  ->  ( ph  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl7bi  221  syl3an3  1217  ax10lem4  1881  hbae  1893  hbae-o  2092  ax11  2094  tz7.7  4418  fvmptt  5615  f1oweALT  5851  nneneq  7044  pr2nelem  7634  cfcoflem  7898  nnunb  9961  ndvdssub  12606  lsmcv  15894  2ndcsep  17185  atcvat4i  22977  mdsymlem5  22987  sumdmdii  22995  dfon2lem6  24144  wfrlem12  24267  frrlem11  24293  colineardim1  24684  lvsovso  25626  icmpmon  25816  eel2122old  28497  ax10lem18ALT  29124  a12study  29132  a12study3  29135  cvrat4  29632  llncvrlpln2  29746  lplncvrlvol2  29804  dihmeetlem3N  31495
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator