Metamath Proof Explorer

Theorem re2luk1

Description: luk-1 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion re2luk1 ⊢ φ → ψ → ψ → χ → φ → χ

Proof

Step Hyp Ref Expression
1 rb-imdf ⊢ ¬ ¬ ¬ ψ → χ → φ → χ ∨ ¬ ψ → χ ∨ φ → χ ∨ ¬ ¬ ¬ ψ → χ ∨ φ → χ ∨ ψ → χ → φ → χ
2 1 rblem7 ⊢ ¬ ¬ ψ → χ ∨ φ → χ ∨ ψ → χ → φ → χ
3 rb-imdf ⊢ ¬ ¬ ¬ ψ → χ ∨ ¬ ψ ∨ χ ∨ ¬ ¬ ¬ ψ ∨ χ ∨ ψ → χ
4 3 rblem6 ⊢ ¬ ψ → χ ∨ ¬ ψ ∨ χ
5 rb-ax2 ⊢ ¬ ¬ ψ → χ ∨ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ψ → χ
6 rb-ax4 ⊢ ¬ ¬ ψ → χ ∨ ¬ ψ → χ ∨ ¬ ψ → χ
7 rb-ax3 ⊢ ¬ ¬ ψ → χ ∨ ¬ ψ → χ ∨ ¬ ψ → χ
8 6 7 rbsyl ⊢ ¬ ¬ ψ → χ ∨ ¬ ψ → χ
9 rb-ax4 ⊢ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ψ ∨ χ
10 rb-ax3 ⊢ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ψ ∨ χ
11 9 10 rbsyl ⊢ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ψ ∨ χ
12 rb-ax2 ⊢ ¬ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ¬ ψ ∨ χ
13 11 12 anmp ⊢ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ¬ ψ ∨ χ
14 8 13 rblem1 ⊢ ¬ ¬ ψ → χ ∨ ¬ ψ ∨ χ ∨ ¬ ψ → χ ∨ ¬ ¬ ¬ ψ ∨ χ
15 5 14 rbsyl ⊢ ¬ ¬ ψ → χ ∨ ¬ ψ ∨ χ ∨ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ψ → χ
16 4 15 anmp ⊢ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ψ → χ
17 rb-imdf ⊢ ¬ ¬ ¬ φ → χ ∨ ¬ φ ∨ χ ∨ ¬ ¬ ¬ φ ∨ χ ∨ φ → χ
18 17 rblem7 ⊢ ¬ ¬ φ ∨ χ ∨ φ → χ
19 16 18 rblem1 ⊢ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ φ ∨ χ ∨ ¬ ψ → χ ∨ φ → χ
20 rb-ax1 ⊢ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ φ ∨ χ
21 rb-ax2 ⊢ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ φ ∨ χ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ χ ∨ ¬ φ ∨ χ
22 rb-ax4 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ
23 rb-ax3 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ
24 22 23 rbsyl ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ
25 rb-ax4 ⊢ ¬ ¬ φ ∨ χ ∨ ¬ φ ∨ χ ∨ ¬ φ ∨ χ
26 rb-ax3 ⊢ ¬ ¬ φ ∨ χ ∨ ¬ φ ∨ χ ∨ ¬ φ ∨ χ
27 25 26 rbsyl ⊢ ¬ ¬ φ ∨ χ ∨ ¬ φ ∨ χ
28 24 27 11 rblem4 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ φ ∨ χ ∨ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ ψ ∨ χ ∨ ¬ φ ∨ χ ∨ ¬ ¬ φ ∨ ψ
29 rb-ax2 ⊢ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ φ ∨ χ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ φ ∨ χ ∨ ¬ ¬ ψ ∨ χ
30 28 29 rbsyl ⊢ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ φ ∨ χ ∨ ¬ ¬ ψ ∨ χ ∨ ¬ φ ∨ χ ∨ ¬ ¬ φ ∨ ψ
31 21 30 rbsyl ⊢ ¬ ¬ ¬ ψ ∨ χ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ φ ∨ χ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ χ ∨ ¬ φ ∨ χ
32 20 31 anmp ⊢ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ χ ∨ ¬ φ ∨ χ
33 19 32 rbsyl ⊢ ¬ ¬ φ ∨ ψ ∨ ¬ ψ → χ ∨ φ → χ
34 rb-imdf ⊢ ¬ ¬ ¬ φ → ψ ∨ ¬ φ ∨ ψ ∨ ¬ ¬ ¬ φ ∨ ψ ∨ φ → ψ
35 34 rblem6 ⊢ ¬ φ → ψ ∨ ¬ φ ∨ ψ
36 33 35 rbsyl ⊢ ¬ φ → ψ ∨ ¬ ψ → χ ∨ φ → χ
37 2 36 rbsyl ⊢ ¬ φ → ψ ∨ ψ → χ → φ → χ
38 rb-imdf ⊢ ¬ ¬ ¬ φ → ψ → ψ → χ → φ → χ ∨ ¬ φ → ψ ∨ ψ → χ → φ → χ ∨ ¬ ¬ ¬ φ → ψ ∨ ψ → χ → φ → χ ∨ φ → ψ → ψ → χ → φ → χ
39 38 rblem7 ⊢ ¬ ¬ φ → ψ ∨ ψ → χ → φ → χ ∨ φ → ψ → ψ → χ → φ → χ
40 37 39 anmp ⊢ φ → ψ → ψ → χ → φ → χ