Metamath Proof Explorer

Theorem re2luk3

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

This theorem, along with re1axmp , re2luk1 , and re2luk2 shows that rb-ax1 , rb-ax2 , rb-ax3 , and rb-ax4 , along with anmp , 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.)

Ref Expression
Assertion re2luk3 ⊢ φ → ¬ φ → ψ

Proof

Step Hyp Ref Expression
1 rb-imdf ⊢ ¬ ¬ ¬ ¬ φ → ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ φ → ψ
2 1 rblem7 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ φ → ψ
3 rb-ax4 ⊢ ¬ ¬ φ ∨ ¬ φ ∨ ¬ φ
4 rb-ax3 ⊢ ¬ ¬ φ ∨ ¬ φ ∨ ¬ φ
5 3 4 rbsyl ⊢ ¬ ¬ φ ∨ ¬ φ
6 rb-ax2 ⊢ ¬ ¬ ¬ φ ∨ ¬ φ ∨ ¬ φ ∨ ¬ ¬ φ
7 5 6 anmp ⊢ ¬ φ ∨ ¬ ¬ φ
8 rblem2 ⊢ ¬ ¬ φ ∨ ¬ ¬ φ ∨ ¬ φ ∨ ¬ ¬ φ ∨ ψ
9 7 8 anmp ⊢ ¬ φ ∨ ¬ ¬ φ ∨ ψ
10 2 9 rbsyl ⊢ ¬ φ ∨ ¬ φ → ψ
11 rb-imdf ⊢ ¬ ¬ ¬ φ → ¬ φ → ψ ∨ ¬ φ ∨ ¬ φ → ψ ∨ ¬ ¬ ¬ φ ∨ ¬ φ → ψ ∨ φ → ¬ φ → ψ
12 11 rblem7 ⊢ ¬ ¬ φ ∨ ¬ φ → ψ ∨ φ → ¬ φ → ψ
13 10 12 anmp ⊢ φ → ¬ φ → ψ