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

Theorem syl8 70
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 69 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com45  89  syl8ib  231  imp5a  598  3exp  1195  mopickOLD  2362  suctr  4961  ssorduni  6605  tfindsg  6679  findsg  6711  tz7.49  7110  nneneq  7700  dfac2  8511  qreccl  11202  cmpsub  19694  bwthOLD  19705  fclsopni  20279  wlkdvspthlem  24313  sumdmdlem2  27042  nocvxminlem  29055  idinside  29339  a1i4  29719  prtlem15  30248  prtlem17  30249  ee3bir  32369  ee233  32386  onfrALTlem2  32416  ee223  32518  eel32131  32607  ee33VD  32777
  Copyright terms: Public domain W3C validator