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  256  mo4  2567  ssorduni  7727  tz7.49  8378  nneneq  9134  dfac2b  10047  qreccl  12913  dvdsaddre2b  16270  cmpsub  23378  fclsopni  23993  nocvxminlem  27763  sumdmdlem2  32508  umgr2cycllem  35341  idinside  36285  axc11n11r  36999  isbasisrelowllem1  37688  isbasisrelowllem2  37689  dmqseqim2  39080  disjlem17  39240  prtlem15  39338  prtlem17  39339  ee3bir  44951  ee233  44967  onfrALTlem2  44994  ee223  45082  ee33VD  45326  ormkglobd  47324  rngccatidALTV  48763  ringccatidALTV  48797