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  imp5aOLD  438  3expOLD  1429  3imp3i2anOLD  1437  suctrOLD  5952  ssorduni  7132  tfindsg  7207  findsg  7240  tz7.49  7693  nneneq  8299  dfac2b  9153  dfac2OLD  9155  qreccl  12011  dvdsaddre2b  15238  cmpsub  21424  fclsopni  22039  sumdmdlem2  29618  nocvxminlem  32230  idinside  32528  axc11n11r  33010  isbasisrelowllem1  33540  isbasisrelowllem2  33541  prtlem15  34683  prtlem17  34684  ee3bir  39234  ee233  39250  onfrALTlem2  39286  ee223  39384  ee33VD  39637  rngccatidALTV  42517  ringccatidALTV  42580
  Copyright terms: Public domain W3C validator