Theorem re2luk3 1532

Description: luk-3 1422 derived from Russell-Bernays'.

This theorem, along with re1axmp 1529, re2luk1 1530, and re2luk2 1531 shows that rb-ax1 1517, rb-ax2 1518, rb-ax3 1519, and rb-ax4 1520, along with anmp 1516, can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Proof of Theorem re2luk3

Step	Hyp	Ref	Expression
1		rb-imdf 1515	. . . 4 ⊢ ¬ (¬ (¬ (¬ φ → ψ) ∨ (¬ ¬ φ ∨ ψ)) ∨ ¬ (¬ (¬ ¬ φ ∨ ψ) ∨ (¬ φ → ψ)))
2	1	rblem7 1528	. . 3 ⊢ (¬ (¬ ¬ φ ∨ ψ) ∨ (¬ φ → ψ))
3		rb-ax4 1520	. . . . . 6 ⊢ (¬ (¬ φ ∨ ¬ φ) ∨ ¬ φ)
4		rb-ax3 1519	. . . . . 6 ⊢ (¬ ¬ φ ∨ (¬ φ ∨ ¬ φ))
5	3, 4	rbsyl 1521	. . . . 5 ⊢ (¬ ¬ φ ∨ ¬ φ)
6		rb-ax2 1518	. . . . 5 ⊢ (¬ (¬ ¬ φ ∨ ¬ φ) ∨ (¬ φ ∨ ¬ ¬ φ))
7	5, 6	anmp 1516	. . . 4 ⊢ (¬ φ ∨ ¬ ¬ φ)
8		rblem2 1523	. . . 4 ⊢ (¬ (¬ φ ∨ ¬ ¬ φ) ∨ (¬ φ ∨ (¬ ¬ φ ∨ ψ)))
9	7, 8	anmp 1516	. . 3 ⊢ (¬ φ ∨ (¬ ¬ φ ∨ ψ))
10	2, 9	rbsyl 1521	. 2 ⊢ (¬ φ ∨ (¬ φ → ψ))
11		rb-imdf 1515	. . 3 ⊢ ¬ (¬ (¬ (φ → (¬ φ → ψ)) ∨ (¬ φ ∨ (¬ φ → ψ))) ∨ ¬ (¬ (¬ φ ∨ (¬ φ → ψ)) ∨ (φ → (¬ φ → ψ))))
12	11	rblem7 1528	. 2 ⊢ (¬ (¬ φ ∨ (¬ φ → ψ)) ∨ (φ → (¬ φ → ψ)))
13	10, 12	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)