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  2653  isofrlem  7371  kmlem9  10264  squeeze0  12247  lcmfunsnlem1  16841  rnglidlmcl  21525  fgss2  24223  onprcf1acwevdlem1  36045  ordcmp  37413  linepsubN  41001  pmapsub  41017  relpfrlem  46138  ichreuopeq  48760  bgoldbnnsum3prm  49107  uhgrimedgi  49193  grimedg  49238