Theorem re2luk2 1531

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

Assertion

Ref	Expression
re2luk2	⊢ ((¬ φ → φ) → φ)

Proof of Theorem re2luk2

Step	Hyp	Ref	Expression
1		rb-ax4 1520	. . . 4 ⊢ (¬ (φ ∨ φ) ∨ φ)
2		rb-ax3 1519	. . . . . . 7 ⊢ (¬ φ ∨ (φ ∨ φ))
3	1, 2	rbsyl 1521	. . . . . 6 ⊢ (¬ φ ∨ φ)
4		rb-ax4 1520	. . . . . . . . 9 ⊢ (¬ (¬ ¬ φ ∨ ¬ ¬ φ) ∨ ¬ ¬ φ)
5		rb-ax3 1519	. . . . . . . . 9 ⊢ (¬ ¬ ¬ φ ∨ (¬ ¬ φ ∨ ¬ ¬ φ))
6	4, 5	rbsyl 1521	. . . . . . . 8 ⊢ (¬ ¬ ¬ φ ∨ ¬ ¬ φ)
7		rb-ax2 1518	. . . . . . . 8 ⊢ (¬ (¬ ¬ ¬ φ ∨ ¬ ¬ φ) ∨ (¬ ¬ φ ∨ ¬ ¬ ¬ φ))
8	6, 7	anmp 1516	. . . . . . 7 ⊢ (¬ ¬ φ ∨ ¬ ¬ ¬ φ)
9	8, 3	rblem1 1522	. . . . . 6 ⊢ (¬ (¬ φ ∨ φ) ∨ (¬ ¬ ¬ φ ∨ φ))
10	3, 9	anmp 1516	. . . . 5 ⊢ (¬ ¬ ¬ φ ∨ φ)
11	10, 3	rblem1 1522	. . . 4 ⊢ (¬ (¬ ¬ φ ∨ φ) ∨ (φ ∨ φ))
12	1, 11	rbsyl 1521	. . 3 ⊢ (¬ (¬ ¬ φ ∨ φ) ∨ φ)
13		rb-imdf 1515	. . . 4 ⊢ ¬ (¬ (¬ (¬ φ → φ) ∨ (¬ ¬ φ ∨ φ)) ∨ ¬ (¬ (¬ ¬ φ ∨ φ) ∨ (¬ φ → φ)))
14	13	rblem6 1527	. . 3 ⊢ (¬ (¬ φ → φ) ∨ (¬ ¬ φ ∨ φ))
15	12, 14	rbsyl 1521	. 2 ⊢ (¬ (¬ φ → φ) ∨ φ)
16		rb-imdf 1515	. . 3 ⊢ ¬ (¬ (¬ ((¬ φ → φ) → φ) ∨ (¬ (¬ φ → φ) ∨ φ)) ∨ ¬ (¬ (¬ (¬ φ → φ) ∨ φ) ∨ ((¬ φ → φ) → φ)))
17	16	rblem7 1528	. 2 ⊢ (¬ (¬ (¬ φ → φ) ∨ φ) ∨ ((¬ φ → φ) → φ))
18	15, 17	anmp 1516	1 ⊢ ((¬ φ → φ) → φ)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 357

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360

This theorem is used by: (None)