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

Theorem syl8 76
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 (𝜑 → (𝜓 → (𝜒𝜃)))
syl8.2 (𝜃𝜏)
Assertion
Ref Expression
syl8 (𝜑 → (𝜓 → (𝜒𝜏)))

Proof of Theorem syl8
StepHypRef Expression
1 syl8.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 syl8.2 . . 3 (𝜃𝜏)
32a1i 11 . 2 (𝜑 → (𝜃𝜏))
41, 3syl6d 75 1 (𝜑 → (𝜓 → (𝜒𝜏)))
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:  a1ddd  80  com45  97  syl8ib  246  imp5a  623  3exp  1283  3imp3i2anOLD  1300  nfimt  1861  suctrOLD  5847  ssorduni  7027  tfindsg  7102  findsg  7135  tz7.49  7585  nneneq  8184  dfac2  8991  qreccl  11846  dvdsaddre2b  15076  cmpsub  21251  fclsopni  21866  sumdmdlem2  29406  nocvxminlem  32018  idinside  32316  axc11n11r  32798  isbasisrelowllem1  33333  isbasisrelowllem2  33334  prtlem15  34479  prtlem17  34480  ee3bir  39026  ee233  39042  onfrALTlem2  39078  ee223  39176  ee33VD  39429  rngccatidALTV  42314  ringccatidALTV  42377
  Copyright terms: Public domain W3C validator