Metamath Proof Explorer

Theorem adh-jarrsc

Description: Replacement of a nested antecedent with an outer antecedent. Commuted simplificated form of elimination of a nested antecedent. Also holds intuitionistically. Polish prefix notation: CCCpqrCsCqr . (Contributed by ADH, 10-Nov-2023) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	adh-jarrsc	$⊢ ((φ \to ψ) \to χ) \to (θ \to (ψ \to χ))$

Proof

Step	Hyp	Ref	Expression
1		jarr	$⊢ ((φ \to ψ) \to χ) \to (ψ \to χ)$
2		ax-1	$⊢ (((φ \to ψ) \to χ) \to (ψ \to χ)) \to (θ \to (((φ \to ψ) \to χ) \to (ψ \to χ)))$
3	1 2	ax-mp	$⊢ θ \to (((φ \to ψ) \to χ) \to (ψ \to χ))$
4		pm2.04	$⊢ (θ \to (((φ \to ψ) \to χ) \to (ψ \to χ))) \to (((φ \to ψ) \to χ) \to (θ \to (ψ \to χ)))$
5	3 4	ax-mp	$⊢ ((φ \to ψ) \to χ) \to (θ \to (ψ \to χ))$