Theorem syl5d 73

Description: A nested syllogism deduction. Deduction associated with syl5 34. (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 25	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜒)))
3		syl5d.2	. 2 ⊢ (𝜑 → (𝜃 → (𝜒 → 𝜏)))
4	2, 3	syldd 72	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  74  syl9  77  imim12d  81  mopick  2651  isofrlem  7320  kmlem9  10112  squeeze0  12092  lcmfunsnlem1  16654  rnglidlmcl  21266  fgss2  23914  ordcmp  36771  linepsubN  40340  pmapsub  40356  relpfrlem  45493  ichreuopeq  48043  bgoldbnnsum3prm  48390  uhgrimedgi  48476  grimedg  48521