Theorem syl10

Description: A nested syllogism inference. (Contributed by Alan Sare, 17-Jul-2011)

	Ref	Expression
Hypotheses	syl10.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
	syl10.2	⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜏 ) ) )
	syl10.3	⊢ ( 𝜒 → ( 𝜏 → 𝜂 ) )
Assertion	syl10	⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜂 ) ) )

Proof

Step	Hyp	Ref	Expression
1		syl10.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		syl10.2	⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜏 ) ) )
3		syl10.3	⊢ ( 𝜒 → ( 𝜏 → 𝜂 ) )
4	1 3	syl6	⊢ ( 𝜑 → ( 𝜓 → ( 𝜏 → 𝜂 ) ) )
5	2 4	syldd	⊢ ( 𝜑 → ( 𝜓 → ( 𝜃 → 𝜂 ) ) )