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  2624  isofrlem  7361  kmlem9  10200  squeeze0  12172  lcmfunsnlem1  16675  rnglidlmcl  21227  fgss2  23883  ordcmp  36449  linepsubN  39755  pmapsub  39771  relpfrlem  44979  ichreuopeq  47465  bgoldbnnsum3prm  47796  grimedg  47908