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  256  mo4  2566  ssorduni  7799  tz7.49  8485  nneneq  9246  nneneqOLD  9258  dfac2b  10171  qreccl  13011  dvdsaddre2b  16344  cmpsub  23408  fclsopni  24023  nocvxminlem  27822  sumdmdlem2  32438  umgr2cycllem  35145  idinside  36085  axc11n11r  36684  isbasisrelowllem1  37356  isbasisrelowllem2  37357  dmqseqim2  38658  disjlem17  38800  prtlem15  38876  prtlem17  38877  ee3bir  44523  ee233  44539  onfrALTlem2  44566  ee223  44654  ee33VD  44899  ormkglobd  46890  rngccatidALTV  48188  ringccatidALTV  48222
  Copyright terms: Public domain W3C validator