Theorem eel12131

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

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

Proof

Step	Hyp	Ref	Expression
1		eel12131.1	$$⊢\phi \to \psi$$
2		eel12131.2	$$⊢\left(\phi \wedge \chi \right)\to \theta$$
3		eel12131.3	$$⊢\left(\phi \wedge \tau \right)\to \eta$$
4		eel12131.4	$$⊢\left(\psi \wedge \theta \wedge \eta \right)\to \zeta$$
5	4	3exp	$$⊢\psi \to \left(\theta \to \left(\eta \to \zeta \right)\right)$$
6	1 2 5	syl2imc	$$⊢\left(\phi \wedge \chi \right)\to \left(\phi \to \left(\eta \to \zeta \right)\right)$$
7	6	ex	$$⊢\phi \to \left(\chi \to \left(\phi \to \left(\eta \to \zeta \right)\right)\right)$$
8	7	pm2.43b	$$⊢\chi \to \left(\phi \to \left(\eta \to \zeta \right)\right)$$
9	8	com13	$$⊢\eta \to \left(\phi \to \left(\chi \to \zeta \right)\right)$$
10	3 9	syl	$$⊢\left(\phi \wedge \tau \right)\to \left(\phi \to \left(\chi \to \zeta \right)\right)$$
11	10	ex	$$⊢\phi \to \left(\tau \to \left(\phi \to \left(\chi \to \zeta \right)\right)\right)$$
12	11	pm2.43b	$$⊢\tau \to \left(\phi \to \left(\chi \to \zeta \right)\right)$$
13	12	3imp231	$$⊢\left(\phi \wedge \chi \wedge \tau \right)\to \zeta$$