Theorem eel00000

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

	Ref	Expression
Hypotheses	eel00000.1	$$⊢\phi$$
	eel00000.2	$$⊢\psi$$
	eel00000.3	$$⊢\chi$$
	eel00000.4	$$⊢\theta$$
	eel00000.5	$$⊢\tau$$
	eel00000.6	$$⊢\left(\left(\left(\left(\phi \wedge \psi \right)\wedge \chi \right)\wedge \theta \right)\wedge \tau \right)\to \eta$$
Assertion	eel00000	$$⊢\eta$$

Proof

Step	Hyp	Ref	Expression
1		eel00000.1	$$⊢\phi$$
2		eel00000.2	$$⊢\psi$$
3		eel00000.3	$$⊢\chi$$
4		eel00000.4	$$⊢\theta$$
5		eel00000.5	$$⊢\tau$$
6		eel00000.6	$$⊢\left(\left(\left(\left(\phi \wedge \psi \right)\wedge \chi \right)\wedge \theta \right)\wedge \tau \right)\to \eta$$
7	6	exp41	$$⊢\left(\phi \wedge \psi \right)\to \left(\chi \to \left(\theta \to \left(\tau \to \eta \right)\right)\right)$$
8	1 7	mpan	$$⊢\psi \to \left(\chi \to \left(\theta \to \left(\tau \to \eta \right)\right)\right)$$
9	2 3 8	mp2	$$⊢\theta \to \left(\tau \to \eta \right)$$
10	4 5 9	mp2	$$⊢\eta$$