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	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-1	⊢ ( 𝜓 → ( 𝜑 → 𝜓 ) )
2	1	imim1i	⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( 𝜓 → 𝜒 ) )