Metamath Proof Explorer

Theorem eel11111

Description: Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017)

	Ref	Expression
Hypotheses	eel11111.1	$⊢ φ \to ψ$
	eel11111.2	$⊢ φ \to χ$
	eel11111.3	$⊢ φ \to θ$
	eel11111.4	$⊢ φ \to τ$
	eel11111.5	$⊢ φ \to η$
	eel11111.6	$⊢ ((((ψ \land χ) \land θ) \land τ) \land η) \to ζ$
Assertion	eel11111	$⊢ φ \to ζ$

Proof

Step	Hyp	Ref	Expression
1		eel11111.1	$⊢ φ \to ψ$
2		eel11111.2	$⊢ φ \to χ$
3		eel11111.3	$⊢ φ \to θ$
4		eel11111.4	$⊢ φ \to τ$
5		eel11111.5	$⊢ φ \to η$
6		eel11111.6	$⊢ ((((ψ \land χ) \land θ) \land τ) \land η) \to ζ$
7	6	exp41	$⊢ (ψ \land χ) \to (θ \to (τ \to (η \to ζ)))$
8	7	ex	$⊢ ψ \to (χ \to (θ \to (τ \to (η \to ζ))))$
9	1 2 3 8	syl3c	$⊢ φ \to (τ \to (η \to ζ))$
10	4 5 9	mp2d	$⊢ φ \to ζ$