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  2591  ssorduni  7793  tz7.49  8456  nneneq  9222  dfac2b  10210  qreccl  13098  dvdsaddre2b  16478  cmpsub  23719  fclsopni  24335  nocvxminlem  28141  umgr2cycllem  30747  sumdmdlem2  33022  idinside  36924  axc11n11r  37660  isbasisrelowllem1  38354  isbasisrelowllem2  38355  dmqseqim2  39750  disjlem17  39910  prtlem15  40008  prtlem17  40009  ee3bir  45562  ee233  45578  onfrALTlem2  45605  ee223  45693  ee33VD  45937  ormkglobd  47963  rngccatidALTV  49445  ringccatidALTV  49479