impsingle-step15

Description: Derivation of impsingle-step15 from ax-mp and impsingle . It is used as a lemma in proofs of imim1 and peirce from impsingle . It is Step 15 in Lukasiewicz, where it appears as 'CCCrqCspCCrpCsp' 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-step15	$⊢ ((φ \to ψ) \to (χ \to θ)) \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 τ))$
3		impsingle	$⊢ ((((φ \to θ) \to (χ \to θ)) \to η) \to ((θ \to λ) \to φ)) \to ((((θ \to λ) \to φ) \to ((φ \to θ) \to (χ \to θ))) \to (((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ))))$
4		impsingle	$⊢ (((χ \to θ) \to ζ) \to (φ \to ψ)) \to (((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ)))$
5		impsingle-step8	$⊢ ((((χ \to θ) \to ζ) \to (φ \to ψ)) \to (((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ)))) \to ((φ \to ψ) \to (((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ))))$
6	4 5	ax-mp	$⊢ (φ \to ψ) \to (((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ)))$
7		impsingle	$⊢ ((φ \to ψ) \to (((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ)))) \to (((((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ))) \to φ) \to ((θ \to λ) \to φ))$
8	6 7	ax-mp	$⊢ ((((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ))) \to φ) \to ((θ \to λ) \to φ)$
9		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 ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ)))))$
10	8 9	ax-mp	$⊢ (((θ \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 θ))))$
11		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 (χ \to θ))) \to (((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ)))) \to ((θ \to λ) \to φ)) \to ((((φ \to θ) \to (χ \to θ)) \to η) \to ((θ \to λ) \to φ)))$
12	10 11	ax-mp	$⊢ (((((θ \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 φ))$
13		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 ((θ \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 θ))))))$
14	12 13	ax-mp	$⊢ (((((φ \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 ((φ \to θ) \to (χ \to θ)))))$
15	3 14	ax-mp	$⊢ (((τ \to σ) \to ρ) \to ((ρ \to τ) \to (μ \to τ))) \to ((((θ \to λ) \to φ) \to ((φ \to θ) \to (χ \to θ))) \to (((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ))))$
16	2 15	ax-mp	$⊢ (((θ \to λ) \to φ) \to ((φ \to θ) \to (χ \to θ))) \to (((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ)))$
17	1 16	ax-mp	$⊢ ((φ \to ψ) \to (χ \to θ)) \to ((φ \to θ) \to (χ \to θ))$

Metamath Proof Explorer

Theorem impsingle-step15

Proof