Theorem mpsyl4anc

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

	Ref	Expression
Hypotheses	mpsyl4anc.1	⊢ 𝜑
	mpsyl4anc.2	⊢ 𝜓
	mpsyl4anc.3	⊢ 𝜒
	mpsyl4anc.4	⊢ ( 𝜃 → 𝜏 )
	mpsyl4anc.5	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜏 ) → 𝜂 )
Assertion	mpsyl4anc	⊢ ( 𝜃 → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		mpsyl4anc.1	⊢ 𝜑
2		mpsyl4anc.2	⊢ 𝜓
3		mpsyl4anc.3	⊢ 𝜒
4		mpsyl4anc.4	⊢ ( 𝜃 → 𝜏 )
5		mpsyl4anc.5	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜏 ) → 𝜂 )
6	1	a1i	⊢ ( 𝜃 → 𝜑 )
7	2	a1i	⊢ ( 𝜃 → 𝜓 )
8	3	a1i	⊢ ( 𝜃 → 𝜒 )
9	6 7 8 4 5	syl1111anc	⊢ ( 𝜃 → 𝜂 )