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

Theorem syl8 65
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 10 . 2  |-  ( ph  ->  ( th  ->  ta ) )
41, 3syl6d 64 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com45  83  syl8ib  222  imp5a  581  3exp  1150  suctr  4491  ssorduni  4593  tfindsg  4667  findsg  4699  tz7.49  6473  nneneq  7060  dfac2  7773  qreccl  10352  cmpsub  17143  fclsopni  17726  sumdmdlem2  23015  nocvxminlem  24415  idinside  24779  prj1b  25182  prj3  25183  bwt2  25695  a1i4  26304  prtlem15  26846  prtlem17  26847  wlkdvspthlem  28365  ee3bir  28563  ee233  28580  onfrALTlem2  28610  ee223  28711  eel32131  28801  ee33VD  28971  a12studyALT  29755
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator