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  7733  tz7.49  8384  nneneq  9140  dfac2b  10053  qreccl  12919  dvdsaddre2b  16276  cmpsub  23365  fclsopni  23980  nocvxminlem  27746  sumdmdlem2  32490  umgr2cycllem  35322  idinside  36266  axc11n11r  36980  isbasisrelowllem1  37671  isbasisrelowllem2  37672  dmqseqim2  39063  disjlem17  39223  prtlem15  39321  prtlem17  39322  ee3bir  44930  ee233  44946  onfrALTlem2  44973  ee223  45061  ee33VD  45305  ormkglobd  47305  rngccatidALTV  48748  ringccatidALTV  48782