Theorem syl5d 74

Description: A nested syllogism deduction. Deduction associated with syl5 35. (Contributed by NM, 14-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) (Proof shortened by Mel L. O'Cat, 2-Feb-2006.)

Hypotheses

Ref	Expression
syl5d.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl5d.2	⊢ (𝜑 → (𝜃 → (𝜒 → 𝜏)))

Assertion

Ref	Expression
syl5d	⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

Proof of Theorem syl5d

Step	Hyp	Ref	Expression
1		syl5d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒)))
3		syl5d.2	. 2 ⊢ (𝜑 → (𝜃 → (𝜒 → 𝜏)))
4	2, 3	syldd 73	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:  syl7  75  syl9  78  imim12d  82  mopick  2650  isofrlem  7348  kmlem9  10240  squeeze0  12223  lcmfunsnlem1  16817  rnglidlmcl  21500  fgss2  24198  onprcf1acwevdlem1  35964  ordcmp  37327  linepsubN  40902  pmapsub  40918  relpfrlem  46036  ichreuopeq  48648  bgoldbnnsum3prm  48995  uhgrimedgi  49081  grimedg  49126