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  257  mo4  2570  ssorduni  7722  tz7.49  8374  nneneq  9130  dfac2b  10044  qreccl  12910  dvdsaddre2b  16267  cmpsub  23383  fclsopni  23998  nocvxminlem  27764  sumdmdlem2  32508  umgr2cycllem  35368  idinside  36312  axc11n11r  37026  isbasisrelowllem1  37717  isbasisrelowllem2  37718  dmqseqim2  39109  disjlem17  39269  prtlem15  39367  prtlem17  39368  ee3bir  44947  ee233  44963  onfrALTlem2  44990  ee223  45078  ee33VD  45322  ormkglobd  47320  rngccatidALTV  48763  ringccatidALTV  48797