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  1196  mopickOLD  2343  suctr  4951  ssorduni  6606  tfindsg  6680  findsg  6712  tz7.49  7112  nneneq  7702  dfac2  8514  qreccl  11212  cmpsub  19877  bwthOLD  19888  fclsopni  20493  wlkdvspthlem  24585  sumdmdlem2  27314  nocvxminlem  29425  idinside  29709  a1i4  30089  prtlem15  30591  prtlem17  30592  rngccatidOLD  32537  ringccatidOLD  32597  ee3bir  33005  ee233  33022  onfrALTlem2  33051  ee223  33153  eel32131  33242  ee33VD  33412
  Copyright terms: Public domain W3C validator