Theorem eel12131

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017)

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

Proof

Step	Hyp	Ref	Expression
1		eel12131.1	⊢ ( 𝜑 → 𝜓 )
2		eel12131.2	⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝜃 )
3		eel12131.3	⊢ ( ( 𝜑 ∧ 𝜏 ) → 𝜂 )
4		eel12131.4	⊢ ( ( 𝜓 ∧ 𝜃 ∧ 𝜂 ) → 𝜁 )
5	4	3exp	⊢ ( 𝜓 → ( 𝜃 → ( 𝜂 → 𝜁 ) ) )
6	1 2 5	syl2imc	⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝜑 → ( 𝜂 → 𝜁 ) ) )
7	6	ex	⊢ ( 𝜑 → ( 𝜒 → ( 𝜑 → ( 𝜂 → 𝜁 ) ) ) )
8	7	pm2.43b	⊢ ( 𝜒 → ( 𝜑 → ( 𝜂 → 𝜁 ) ) )
9	8	com13	⊢ ( 𝜂 → ( 𝜑 → ( 𝜒 → 𝜁 ) ) )
10	3 9	syl	⊢ ( ( 𝜑 ∧ 𝜏 ) → ( 𝜑 → ( 𝜒 → 𝜁 ) ) )
11	10	ex	⊢ ( 𝜑 → ( 𝜏 → ( 𝜑 → ( 𝜒 → 𝜁 ) ) ) )
12	11	pm2.43b	⊢ ( 𝜏 → ( 𝜑 → ( 𝜒 → 𝜁 ) ) )
13	12	3imp231	⊢ ( ( 𝜑 ∧ 𝜒 ∧ 𝜏 ) → 𝜁 )