Theorem syl3anl

Description: A triple syllogism inference. (Contributed by NM, 24-Dec-2006)

	Ref	Expression
Hypotheses	syl3anl.1	⊢ ( 𝜑 → 𝜓 )
	syl3anl.2	⊢ ( 𝜒 → 𝜃 )
	syl3anl.3	⊢ ( 𝜏 → 𝜂 )
	syl3anl.4	⊢ ( ( ( 𝜓 ∧ 𝜃 ∧ 𝜂 ) ∧ 𝜁 ) → 𝜎 )
Assertion	syl3anl	⊢ ( ( ( 𝜑 ∧ 𝜒 ∧ 𝜏 ) ∧ 𝜁 ) → 𝜎 )

Proof

Step	Hyp	Ref	Expression
1		syl3anl.1	⊢ ( 𝜑 → 𝜓 )
2		syl3anl.2	⊢ ( 𝜒 → 𝜃 )
3		syl3anl.3	⊢ ( 𝜏 → 𝜂 )
4		syl3anl.4	⊢ ( ( ( 𝜓 ∧ 𝜃 ∧ 𝜂 ) ∧ 𝜁 ) → 𝜎 )
5	1 2 3	3anim123i	⊢ ( ( 𝜑 ∧ 𝜒 ∧ 𝜏 ) → ( 𝜓 ∧ 𝜃 ∧ 𝜂 ) )
6	5 4	sylan	⊢ ( ( ( 𝜑 ∧ 𝜒 ∧ 𝜏 ) ∧ 𝜁 ) → 𝜎 )