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

Theorem syl8 65
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 10 . 2  |-  ( ph  ->  ( th  ->  ta ) )
41, 3syl6d 64 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com45  83  syl8ib  222  imp5a  581  3exp  1150  suctr  4477  ssorduni  4579  tfindsg  4653  findsg  4685  tz7.49  6459  nneneq  7046  dfac2  7759  qreccl  10338  cmpsub  17129  fclsopni  17712  sumdmdlem2  23001  nocvxminlem  24346  idinside  24709  prj1b  25090  prj3  25091  bwt2  25603  a1i4  26212  prtlem15  26754  prtlem17  26755  ee3bir  28320  ee233  28337  onfrALTlem2  28367  ee223  28468  eel32131  28558  ee33VD  28728  a12studyALT  29206
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator