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

Metamath Proof Explorer

Theorem eel00001

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

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