Theorem eel00000

Description: Elimination rule similar eel0000 , except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017)

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

Proof

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