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

Theorem syl8 67
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 66 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com45  85  syl8ib  223  imp5a  582  3exp  1152  suctrALT  4656  ssorduni  4758  tfindsg  4832  findsg  4864  tz7.49  6694  nneneq  7282  dfac2  8003  qreccl  10586  cmpsub  17455  bwth  17465  fclsopni  18039  wlkdvspthlem  21599  sumdmdlem2  23914  nocvxminlem  25637  idinside  26010  a1i4  26290  prtlem15  26715  prtlem17  26716  ee3bir  28522  ee233  28539  onfrALTlem2  28569  ee223  28672  eel32131  28761  ee33VD  28928
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator