Theorem luklem6

Description: Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	luklem6	⊢ ( ( 𝜑 → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		luk-1	⊢ ( ( 𝜑 → ( 𝜑 → 𝜓 ) ) → ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
2		luklem5	⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( ¬ 𝜓 → ¬ ( 𝜑 → 𝜓 ) ) )
3		luklem2	⊢ ( ( ¬ 𝜓 → ¬ ( 𝜑 → 𝜓 ) ) → ( ( ( ¬ 𝜓 → 𝜓 ) → 𝜓 ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) ) )
4		luklem4	⊢ ( ( ( ( ¬ 𝜓 → 𝜓 ) → 𝜓 ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )
5	3 4	luklem1	⊢ ( ( ¬ 𝜓 → ¬ ( 𝜑 → 𝜓 ) ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )
6	2 5	luklem1	⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )
7		luk-1	⊢ ( ( ¬ ( 𝜑 → 𝜓 ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) ) → ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) ) )
8	6 7	ax-mp	⊢ ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) )
9		luk-1	⊢ ( ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) ) → ( ( ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) ) ) )
10	8 9	ax-mp	⊢ ( ( ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) ) )
11		luklem4	⊢ ( ( ( ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) ) → ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) ) ) → ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) ) )
12	10 11	ax-mp	⊢ ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) )
13	1 12	luklem1	⊢ ( ( 𝜑 → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) )