Metamath Proof Explorer


Theorem 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 φ ψ χ ψ ψ θ φ τ η ψ θ φ τ

Proof

Step Hyp Ref Expression
1 impsingle ψ θ φ φ ψ χ ψ
2 impsingle χ ψ ρ ψ θ φ τ ψ θ φ τ χ ψ φ ψ χ ψ
3 impsingle-step8 χ ψ ρ ψ θ φ τ ψ θ φ τ χ ψ φ ψ χ ψ ψ θ φ τ ψ θ φ τ χ ψ φ ψ χ ψ
4 2 3 ax-mp ψ θ φ τ ψ θ φ τ χ ψ φ ψ χ ψ
5 impsingle-step15 ψ θ φ τ ψ θ φ τ χ ψ φ ψ χ ψ ψ θ φ φ ψ χ ψ ψ θ φ τ χ ψ φ ψ χ ψ
6 4 5 ax-mp ψ θ φ φ ψ χ ψ ψ θ φ τ χ ψ φ ψ χ ψ
7 1 6 ax-mp ψ θ φ τ χ ψ φ ψ χ ψ
8 impsingle ψ θ φ τ χ ψ φ ψ χ ψ φ ψ χ ψ ψ θ φ τ η ψ θ φ τ
9 7 8 ax-mp φ ψ χ ψ ψ θ φ τ η ψ θ φ τ