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

Metamath Proof Explorer

Theorem jarr

Description: Elimination of a nested antecedent. Sometimes called "Syll-Simp" since it is a syllogism applied to ax-1 ("Simplification"). (Contributed by Wolf Lammen, 9-May-2013)

		Ref	Expression
	Assertion	jarr	$⊢ ((φ \to ψ) \to χ) \to (ψ \to χ)$

Proof

Step	Hyp	Ref	Expression
1		ax-1	$⊢ ψ \to (φ \to ψ)$
2	1	imim1i	$⊢ ((φ \to ψ) \to χ) \to (ψ \to χ)$