impsingle-step19

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

Proof

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

Metamath Proof Explorer

Theorem impsingle-step19

Proof