Theorem eel00001

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

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

Proof

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