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  257  mo4  2643  ssorduni  7489  tz7.49  8070  nneneq  8688  dfac2b  9544  qreccl  12356  dvdsaddre2b  15645  cmpsub  21936  fclsopni  22551  sumdmdlem2  30123  umgr2cycllem  32284  nocvxminlem  33144  idinside  33442  axc11n11r  33914  isbasisrelowllem1  34518  isbasisrelowllem2  34519  dmqseqim2  35771  prtlem15  35891  prtlem17  35892  ee3bir  40714  ee233  40730  onfrALTlem2  40757  ee223  40845  ee33VD  41090  rngccatidALTV  44188  ringccatidALTV  44251
  Copyright terms: Public domain W3C validator