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 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl7  75  syl9  78  imim12d  82  mopick  2653  isofrlem  7340  kmlem9  10143  squeeze0  12119  lcmfunsnlem1  16696  rnglidlmcl  21322  fgss2  24012  ordcmp  36936  linepsubN  40504  pmapsub  40520  relpfrlem  45642  ichreuopeq  48199  bgoldbnnsum3prm  48546  uhgrimedgi  48632  grimedg  48677