This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eel00000

Description: Elimination rule similar eel0000 , except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017)

Step	Hyp	Ref	Expression
1		eel00000.1	$⊢ φ$
2		eel00000.2	$⊢ ψ$
3		eel00000.3	$⊢ χ$
4		eel00000.4	$⊢ θ$
5		eel00000.5	$⊢ τ$
6		eel00000.6	$⊢ ((((φ \land ψ) \land χ) \land θ) \land τ) \to η$
7	6	exp41	$⊢ (φ \land ψ) \to (χ \to (θ \to (τ \to η)))$
8	1 7	mpan	$⊢ ψ \to (χ \to (θ \to (τ \to η)))$
9	2 3 8	mp2	$⊢ θ \to (τ \to η)$
10	4 5 9	mp2	$⊢ η$