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  1186  mopickOLD  2340  suctr  4807  ssorduni  6402  tfindsg  6476  findsg  6508  tz7.49  6905  nneneq  7499  dfac2  8305  qreccl  10978  cmpsub  19008  bwthOLD  19019  fclsopni  19593  wlkdvspthlem  23511  sumdmdlem2  25828  nocvxminlem  27836  idinside  28120  a1i4  28496  prtlem15  29025  prtlem17  29026  ee3bir  31212  ee233  31229  onfrALTlem2  31259  ee223  31361  eel32131  31450  ee33VD  31620
  Copyright terms: Public domain W3C validator