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  247  imp5aOLD  440  3expOLD  1438  3imp3i2anOLD  1446  ssorduni  7211  tfindsg  7286  findsg  7319  tz7.49  7772  nneneq  8378  dfac2b  9232  dfac2OLD  9234  qreccl  12023  dvdsaddre2b  15248  cmpsub  21413  fclsopni  22028  sumdmdlem2  29602  nocvxminlem  32209  idinside  32507  axc11n11r  32983  isbasisrelowllem1  33514  isbasisrelowllem2  33515  prtlem15  34649  prtlem17  34650  ee3bir  39201  ee233  39217  onfrALTlem2  39253  ee223  39351  ee33VD  39603  rngccatidALTV  42551  ringccatidALTV  42614
  Copyright terms: Public domain W3C validator