Theorem syl8 77

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 76	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  a1ddd  81  com45  98  syl8ib  259  mo4  2594  ssorduni  7803  tz7.49  8469  nneneq  9235  dfac2b  10222  qreccl  13110  dvdsaddre2b  16492  cmpsub  23733  fclsopni  24349  nocvxminlem  28155  umgr2cycllem  30761  sumdmdlem2  33036  idinside  36979  axc11n11r  37715  isbasisrelowllem1  38421  isbasisrelowllem2  38422  dmqseqim2  39817  disjlem17  39977  prtlem15  40075  prtlem17  40076  ee3bir  45628  ee233  45644  onfrALTlem2  45671  ee223  45759  ee33VD  46003  ormkglobd  48029  rngccatidALTV  49511  ringccatidALTV  49545