impsingle-step25

Description: Derivation of impsingle-step25 from ax-mp and impsingle . It is used as a lemma in the proof of imim1 from impsingle . It is Step 25 in Lukasiewicz, where it appears as 'CCpqCCCprqq' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	impsingle-step25	$⊢ (φ \to ψ) \to (((φ \to χ) \to ψ) \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		impsingle-step22	$⊢ (((φ \to χ) \to ψ) \to ψ) \to (((φ \to χ) \to ψ) \to ψ)$
2		impsingle-step20	$⊢ ((((φ \to χ) \to ψ) \to ψ) \to (((φ \to χ) \to ψ) \to ψ)) \to (((ψ \to θ) \to (φ \to χ)) \to (((φ \to χ) \to ψ) \to ψ))$
3	1 2	ax-mp	$⊢ ((ψ \to θ) \to (φ \to χ)) \to (((φ \to χ) \to ψ) \to ψ)$
4		impsingle-step8	$⊢ (((ψ \to θ) \to (φ \to χ)) \to (((φ \to χ) \to ψ) \to ψ)) \to ((φ \to χ) \to (((φ \to χ) \to ψ) \to ψ))$
5	3 4	ax-mp	$⊢ (φ \to χ) \to (((φ \to χ) \to ψ) \to ψ)$
6		impsingle-step15	$⊢ ((φ \to χ) \to (((φ \to χ) \to ψ) \to ψ)) \to ((φ \to ψ) \to (((φ \to χ) \to ψ) \to ψ))$
7	5 6	ax-mp	$⊢ (φ \to ψ) \to (((φ \to χ) \to ψ) \to ψ)$

Metamath Proof Explorer

Theorem impsingle-step25

Proof