MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl8 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  suctr  4598  ssorduni  4699  tfindsg  4773  findsg  4805  tz7.49  6631  nneneq  7219  dfac2  7937  qreccl  10519  cmpsub  17378  fclsopni  17961  wlkdvspthlem  21448  sumdmdlem2  23763  nocvxminlem  25361  idinside  25725  a1i4  25983  prtlem15  26408  prtlem17  26409  ee3bir  27921  ee233  27938  onfrALTlem2  27968  ee223  28069  eel32131  28158  ee33VD  28325  a12studyALT  29109
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator