impsingle-step8

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

Metamath Proof Explorer

Theorem impsingle-step8

Proof