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  258  mo4  2593  ssorduni  7762  tz7.49  8416  nneneq  9174  dfac2b  10087  qreccl  12970  dvdsaddre2b  16341  cmpsub  23460  fclsopni  24075  nocvxminlem  27847  sumdmdlem2  32622  umgr2cycllem  35490  idinside  36434  axc11n11r  37158  isbasisrelowllem1  37849  isbasisrelowllem2  37850  dmqseqim2  39241  disjlem17  39401  prtlem15  39499  prtlem17  39500  ee3bir  45079  ee233  45095  onfrALTlem2  45122  ee223  45210  ee33VD  45454  ormkglobd  47451  rngccatidALTV  48894  ringccatidALTV  48928