impsingle-step22

Description: Derivation of impsingle-step22 from ax-mp and impsingle . It is used as a lemma in proofs of imim1 and peirce from impsingle . It is Step 22 in Lukasiewicz, where it appears as 'Cpp' 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-step22	$⊢ φ \to φ$

Proof

Step	Hyp	Ref	Expression
1		impsingle-step4	$⊢ ((θ \to μ) \to θ) \to (λ \to θ)$
2		impsingle-step4	$⊢ ((φ \to ψ) \to φ) \to (φ \to φ)$
3		impsingle-step4	$⊢ ((φ \to φ) \to φ) \to ((φ \to ψ) \to φ)$
4		impsingle	$⊢ (((φ \to φ) \to φ) \to ((φ \to ψ) \to φ)) \to ((((φ \to ψ) \to φ) \to (φ \to φ)) \to ((((θ \to μ) \to θ) \to (λ \to θ)) \to (φ \to φ)))$
5	3 4	ax-mp	$⊢ (((φ \to ψ) \to φ) \to (φ \to φ)) \to ((((θ \to μ) \to θ) \to (λ \to θ)) \to (φ \to φ))$
6	2 5	ax-mp	$⊢ (((θ \to μ) \to θ) \to (λ \to θ)) \to (φ \to φ)$
7	1 6	ax-mp	$⊢ φ \to φ$

Metamath Proof Explorer

Theorem impsingle-step22

Proof