Theorem re2luk2

Description: luk-2 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	re2luk2	⊢ ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rb-ax4	⊢ ( ¬ ( 𝜑 ∨ 𝜑 ) ∨ 𝜑 )
2		rb-ax3	⊢ ( ¬ 𝜑 ∨ ( 𝜑 ∨ 𝜑 ) )
3	1 2	rbsyl	⊢ ( ¬ 𝜑 ∨ 𝜑 )
4		rb-ax4	⊢ ( ¬ ( ¬ ¬ 𝜑 ∨ ¬ ¬ 𝜑 ) ∨ ¬ ¬ 𝜑 )
5		rb-ax3	⊢ ( ¬ ¬ ¬ 𝜑 ∨ ( ¬ ¬ 𝜑 ∨ ¬ ¬ 𝜑 ) )
6	4 5	rbsyl	⊢ ( ¬ ¬ ¬ 𝜑 ∨ ¬ ¬ 𝜑 )
7		rb-ax2	⊢ ( ¬ ( ¬ ¬ ¬ 𝜑 ∨ ¬ ¬ 𝜑 ) ∨ ( ¬ ¬ 𝜑 ∨ ¬ ¬ ¬ 𝜑 ) )
8	6 7	anmp	⊢ ( ¬ ¬ 𝜑 ∨ ¬ ¬ ¬ 𝜑 )
9	8 3	rblem1	⊢ ( ¬ ( ¬ 𝜑 ∨ 𝜑 ) ∨ ( ¬ ¬ ¬ 𝜑 ∨ 𝜑 ) )
10	3 9	anmp	⊢ ( ¬ ¬ ¬ 𝜑 ∨ 𝜑 )
11	10 3	rblem1	⊢ ( ¬ ( ¬ ¬ 𝜑 ∨ 𝜑 ) ∨ ( 𝜑 ∨ 𝜑 ) )
12	1 11	rbsyl	⊢ ( ¬ ( ¬ ¬ 𝜑 ∨ 𝜑 ) ∨ 𝜑 )
13		rb-imdf	⊢ ¬ ( ¬ ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( ¬ ¬ 𝜑 ∨ 𝜑 ) ) ∨ ¬ ( ¬ ( ¬ ¬ 𝜑 ∨ 𝜑 ) ∨ ( ¬ 𝜑 → 𝜑 ) ) )
14	13	rblem6	⊢ ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ ( ¬ ¬ 𝜑 ∨ 𝜑 ) )
15	12 14	rbsyl	⊢ ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ 𝜑 )
16		rb-imdf	⊢ ¬ ( ¬ ( ¬ ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 ) ∨ ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ 𝜑 ) ) ∨ ¬ ( ¬ ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ 𝜑 ) ∨ ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 ) ) )
17	16	rblem7	⊢ ( ¬ ( ¬ ( ¬ 𝜑 → 𝜑 ) ∨ 𝜑 ) ∨ ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 ) )
18	15 17	anmp	⊢ ( ( ¬ 𝜑 → 𝜑 ) → 𝜑 )