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  2592  ssorduni  7793  tz7.49  8455  nneneq  9221  dfac2b  10209  qreccl  13097  dvdsaddre2b  16477  cmpsub  23718  fclsopni  24334  nocvxminlem  28140  umgr2cycllem  30746  sumdmdlem2  33021  idinside  36849  axc11n11r  37585  isbasisrelowllem1  38278  isbasisrelowllem2  38279  dmqseqim2  39674  disjlem17  39834  prtlem15  39932  prtlem17  39933  ee3bir  45485  ee233  45501  onfrALTlem2  45528  ee223  45616  ee33VD  45860  ormkglobd  47886  rngccatidALTV  49368  ringccatidALTV  49402