Theorem mpsyl4anc

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

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

Proof

Step	Hyp	Ref	Expression
1		mpsyl4anc.1	$$⊢\phi$$
2		mpsyl4anc.2	$$⊢\psi$$
3		mpsyl4anc.3	$$⊢\chi$$
4		mpsyl4anc.4	$$⊢\theta \to \tau$$
5		mpsyl4anc.5	$$⊢\left(\left(\left(\phi \wedge \psi \right)\wedge \chi \right)\wedge \tau \right)\to \eta$$
6	1	a1i	$$⊢\theta \to \phi$$
7	2	a1i	$$⊢\theta \to \psi$$
8	3	a1i	$$⊢\theta \to \chi$$
9	6 7 8 4 5	syl1111anc	$$⊢\theta \to \eta$$