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  259  mo4  2628  ssorduni  7484  tz7.49  8068  nneneq  8688  dfac2b  9545  qreccl  12360  dvdsaddre2b  15652  cmpsub  22008  fclsopni  22623  sumdmdlem2  30205  umgr2cycllem  32495  nocvxminlem  33355  idinside  33653  axc11n11r  34125  isbasisrelowllem1  34767  isbasisrelowllem2  34768  dmqseqim2  36044  prtlem15  36164  prtlem17  36165  ee3bir  41196  ee233  41212  onfrALTlem2  41239  ee223  41327  ee33VD  41572  rngccatidALTV  44600  ringccatidALTV  44663
  Copyright terms: Public domain W3C validator