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  7779  tz7.49  8437  nneneq  9203  dfac2b  10136  qreccl  13022  dvdsaddre2b  16400  cmpsub  23628  fclsopni  24244  nocvxminlem  28022  umgr2cycllem  30628  sumdmdlem2  32903  idinside  36667  axc11n11r  37419  isbasisrelowllem1  38112  isbasisrelowllem2  38113  dmqseqim2  39493  disjlem17  39653  prtlem15  39751  prtlem17  39752  ee3bir  45329  ee233  45345  onfrALTlem2  45372  ee223  45460  ee33VD  45704  ormkglobd  47708  rngccatidALTV  49190  ringccatidALTV  49224