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

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

Proof of Theorem syl8
StepHypRef Expression
1 syl8.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
2 syl8.2 . . 3  |-  ( th 
->  ta )
32a1i 11 . 2  |-  ( ph  ->  ( th  ->  ta ) )
41, 3syl6d 66 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com45  85  syl8ib  223  imp5a  582  3exp  1152  suctrALT  4664  ssorduni  4766  tfindsg  4840  findsg  4872  tz7.49  6702  nneneq  7290  dfac2  8011  qreccl  10594  cmpsub  17463  bwth  17473  fclsopni  18047  wlkdvspthlem  21607  sumdmdlem2  23922  nocvxminlem  25645  idinside  26018  a1i4  26299  prtlem15  26724  prtlem17  26725  ee3bir  28585  ee233  28602  onfrALTlem2  28632  ee223  28735  eel32131  28824  ee33VD  28991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator