impsingle-step18

Description: Derivation of impsingle-step18 from ax-mp and impsingle . It is used as a lemma in proofs of imim1 and peirce from impsingle . It is Step 18 in Lukasiewicz, where it appears as 'CCCCrpCspCCCpqrtCuCCCpqrt' 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-step18	$⊢ (((φ \to ψ) \to (χ \to ψ)) \to (((ψ \to θ) \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 τ)) \to (((((ψ \to θ) \to φ) \to τ) \to (χ \to ψ)) \to ((φ \to ψ) \to (χ \to ψ)))$
3		impsingle-step8	$⊢ ((((χ \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 ψ)))$
5		impsingle-step15	$⊢ ((((ψ \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 ψ))))$
6	4 5	ax-mp	$⊢ (((ψ \to θ) \to φ) \to ((φ \to ψ) \to (χ \to ψ))) \to (((((ψ \to θ) \to φ) \to τ) \to (χ \to ψ)) \to ((φ \to ψ) \to (χ \to ψ)))$
7	1 6	ax-mp	$⊢ ((((ψ \to θ) \to φ) \to τ) \to (χ \to ψ)) \to ((φ \to ψ) \to (χ \to ψ))$
8		impsingle	$⊢ (((((ψ \to θ) \to φ) \to τ) \to (χ \to ψ)) \to ((φ \to ψ) \to (χ \to ψ))) \to ((((φ \to ψ) \to (χ \to ψ)) \to (((ψ \to θ) \to φ) \to τ)) \to (η \to (((ψ \to θ) \to φ) \to τ)))$
9	7 8	ax-mp	$⊢ (((φ \to ψ) \to (χ \to ψ)) \to (((ψ \to θ) \to φ) \to τ)) \to (η \to (((ψ \to θ) \to φ) \to τ))$

Metamath Proof Explorer

Theorem impsingle-step18

Proof