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  1261  3imp3i2an  1275  nfimt  1818  suctrOLD  5768  ssorduni  6932  tfindsg  7007  findsg  7040  tz7.49  7485  nneneq  8087  dfac2  8897  qreccl  11752  dvdsaddre2b  14953  cmpsub  21113  fclsopni  21729  sumdmdlem2  29124  nocvxminlem  31550  idinside  31830  axc11n11r  32312  isbasisrelowllem1  32832  isbasisrelowllem2  32833  prtlem15  33637  prtlem17  33638  ee3bir  38188  ee233  38204  onfrALTlem2  38240  ee223  38338  ee33VD  38595  rngccatidALTV  41274  ringccatidALTV  41337
  Copyright terms: Public domain W3C validator