Metamath Proof Explorer

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