impsingle-step4

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

Proof

Step	Hyp	Ref	Expression
1		impsingle	$⊢ ((τ \to η) \to ζ) \to ((ζ \to τ) \to (σ \to τ))$
2		impsingle	$⊢ ((φ \to θ) \to (φ \to ψ)) \to (((φ \to ψ) \to φ) \to (χ \to φ))$
3		impsingle	$⊢ ((φ \to ψ) \to (φ \to ψ)) \to (((φ \to ψ) \to φ) \to (χ \to φ))$
4		impsingle	$⊢ (((φ \to ψ) \to (φ \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 ψ))$
6		impsingle	$⊢ (((((φ \to ψ) \to φ) \to (χ \to φ)) \to (φ \to ψ)) \to ((φ \to θ) \to (φ \to ψ))) \to ((((φ \to θ) \to (φ \to ψ)) \to (((φ \to ψ) \to φ) \to (χ \to φ))) \to ((((τ \to η) \to ζ) \to ((ζ \to τ) \to (σ \to τ))) \to (((φ \to ψ) \to φ) \to (χ \to φ))))$
7	5 6	ax-mp	$⊢ (((φ \to θ) \to (φ \to ψ)) \to (((φ \to ψ) \to φ) \to (χ \to φ))) \to ((((τ \to η) \to ζ) \to ((ζ \to τ) \to (σ \to τ))) \to (((φ \to ψ) \to φ) \to (χ \to φ)))$
8	2 7	ax-mp	$⊢ (((τ \to η) \to ζ) \to ((ζ \to τ) \to (σ \to τ))) \to (((φ \to ψ) \to φ) \to (χ \to φ))$
9	1 8	ax-mp	$⊢ ((φ \to ψ) \to φ) \to (χ \to φ)$

Metamath Proof Explorer

Theorem impsingle-step4

Proof