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  4475  ssorduni  4577  tfindsg  4651  findsg  4683  tz7.49  6457  nneneq  7044  dfac2  7757  qreccl  10336  cmpsub  17127  fclsopni  17710  sumdmdlem2  22999  nocvxminlem  23755  idinside  24118  prj1b  24491  prj3  24492  bwt2  25004  a1i4  25613  prtlem15  26155  prtlem17  26156  ee3bir  27637  ee233  27654  onfrALTlem2  27684  ee223  27779  ee33VD  28028  a12studyALT  28506
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator