Theorem eel00001

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

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

Proof

Step	Hyp	Ref	Expression
1		eel00001.1	⊢ 𝜑
2		eel00001.2	⊢ 𝜓
3		eel00001.3	⊢ 𝜒
4		eel00001.4	⊢ 𝜃
5		eel00001.5	⊢ ( 𝜏 → 𝜂 )
6		eel00001.6	⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜂 ) → 𝜁 )
7	6	exp41	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → ( 𝜃 → ( 𝜂 → 𝜁 ) ) ) )
8	1 2 7	mp2an	⊢ ( 𝜒 → ( 𝜃 → ( 𝜂 → 𝜁 ) ) )
9	3 4 8	mp2	⊢ ( 𝜂 → 𝜁 )
10	5 9	syl	⊢ ( 𝜏 → 𝜁 )