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