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  596  3exp  1193  mopickOLD  2354  suctr  4950  ssorduni  6594  tfindsg  6668  findsg  6700  tz7.49  7102  nneneq  7693  dfac2  8502  qreccl  11203  cmpsub  20067  fclsopni  20682  wlkdvspthlem  24811  sumdmdlem2  27536  nocvxminlem  29690  idinside  29962  a1i4  30354  prtlem15  30856  prtlem17  30857  rngccatidALTV  33051  ringccatidALTV  33114  ee3bir  33659  ee233  33676  onfrALTlem2  33712  ee223  33814  eel32131  33903  ee33VD  34080
  Copyright terms: Public domain W3C validator