Theorem luklem4 664

Description: Lemma for rederiving standard propositional axioms from Lukasiewicz'.

Assertion

Ref	Expression
luklem4	⊢ ((((¬ φ → φ) → φ) → ψ) → ψ)

Proof of Theorem luklem4

Step	Hyp	Ref	Expression
1		luk-2 659	. . . 4 ⊢ ((¬ ((¬ φ → φ) → φ) → ((¬ φ → φ) → φ)) → ((¬ φ → φ) → φ))
2		luk-2 659	. . . . 5 ⊢ ((¬ φ → φ) → φ)
3		luklem3 663	. . . . 5 ⊢ (((¬ φ → φ) → φ) → (((¬ ((¬ φ → φ) → φ) → ((¬ φ → φ) → φ)) → ((¬ φ → φ) → φ)) → (¬ ψ → ((¬ φ → φ) → φ))))
4	2, 3	ax-mp 6	. . . 4 ⊢ (((¬ ((¬ φ → φ) → φ) → ((¬ φ → φ) → φ)) → ((¬ φ → φ) → φ)) → (¬ ψ → ((¬ φ → φ) → φ)))
5	1, 4	ax-mp 6	. . 3 ⊢ (¬ ψ → ((¬ φ → φ) → φ))
6		luk-1 658	. . 3 ⊢ ((¬ ψ → ((¬ φ → φ) → φ)) → ((((¬ φ → φ) → φ) → ψ) → (¬ ψ → ψ)))
7	5, 6	ax-mp 6	. 2 ⊢ ((((¬ φ → φ) → φ) → ψ) → (¬ ψ → ψ))
8		luk-2 659	. 2 ⊢ ((¬ ψ → ψ) → ψ)
9	7, 8	luklem1 661	1 ⊢ ((((¬ φ → φ) → φ) → ψ) → ψ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  luklem5 665  luklem6 666  ax3 671

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org