Theorem eel0000

Description: Elimination rule similar to mp4an , except with a left-nested conjunction unification theorem. (Contributed by Alan Sare, 17-Oct-2017)

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

Proof

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