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  255  mo4  2560  ssorduni  7768  tz7.49  8447  nneneq  9211  nneneqOLD  9223  dfac2b  10127  qreccl  12955  dvdsaddre2b  16252  cmpsub  22911  fclsopni  23526  nocvxminlem  27286  sumdmdlem2  31710  umgr2cycllem  34200  idinside  35131  axc11n11r  35653  isbasisrelowllem1  36328  isbasisrelowllem2  36329  dmqseqim2  37619  disjlem17  37761  prtlem15  37837  prtlem17  37838  ee3bir  43352  ee233  43368  onfrALTlem2  43395  ee223  43483  ee33VD  43728  rngccatidALTV  46972  ringccatidALTV  47035