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  2566  ssorduni  7724  tz7.49  8376  nneneq  9130  dfac2b  10041  qreccl  12882  dvdsaddre2b  16234  cmpsub  23344  fclsopni  23959  nocvxminlem  27750  sumdmdlem2  32494  umgr2cycllem  35334  idinside  36278  axc11n11r  36884  isbasisrelowllem1  37560  isbasisrelowllem2  37561  dmqseqim2  38916  disjlem17  39058  prtlem15  39135  prtlem17  39136  ee3bir  44744  ee233  44760  onfrALTlem2  44787  ee223  44875  ee33VD  45119  ormkglobd  47119  rngccatidALTV  48518  ringccatidALTV  48552