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