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 ⊢φ→¬φ→ψ