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

Step	Hyp	Ref	Expression
1		syl8.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2		syl8.2	. . 3 ⊢ (𝜃 → 𝜏)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
4	1, 3	syl6d 75	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))

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  imp5a  623  3exp  1283  3imp3i2anOLD  1300  nfimt  1861  suctrOLD  5847  ssorduni  7027  tfindsg  7102  findsg  7135  tz7.49  7585  nneneq  8184  dfac2  8991  qreccl  11846  dvdsaddre2b  15076  cmpsub  21251  fclsopni  21866  sumdmdlem2  29406  nocvxminlem  32018  idinside  32316  axc11n11r  32798  isbasisrelowllem1  33333  isbasisrelowllem2  33334  prtlem15  34479  prtlem17  34480  ee3bir  39026  ee233  39042  onfrALTlem2  39078  ee223  39176  ee33VD  39429  rngccatidALTV  42314  ringccatidALTV  42377