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

Theorem syl8 74
 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 73 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  78  com45  95  syl8ib  245  imp5a  622  3exp  1256  3imp3i2an  1270  suctrOLD  5726  ssorduni  6877  tfindsg  6952  findsg  6985  tz7.49  7427  nneneq  8028  dfac2  8836  qreccl  11684  dvdsaddre2b  14867  cmpsub  21013  fclsopni  21629  wlkdvspthlem  26137  sumdmdlem2  28662  nocvxminlem  31089  idinside  31361  axc11n11r  31860  bj-nfimt  32025  isbasisrelowllem1  32379  isbasisrelowllem2  32380  prtlem15  33178  prtlem17  33179  ee3bir  37730  ee233  37746  onfrALTlem2  37782  ee223  37880  ee33VD  38137  rngccatidALTV  41781  ringccatidALTV  41844
 Copyright terms: Public domain W3C validator