Metamath Proof Explorer

Theorem usgrexmpl2trifr

Description: G is triangle-free. (Contributed by AV, 10-Aug-2025)

Ref Expression
Hypotheses usgrexmpl2.v ⊢ V = 0 … 5
usgrexmpl2.e ⊢ E = ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
usgrexmpl2.g ⊢ G = V E
Assertion usgrexmpl2trifr Could not format assertion : No typesetting found for |- -. E. t t e. ( GrTriangles ` G ) with typecode |-

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ V = 0 … 5
2 usgrexmpl2.e ⊢ E = ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
3 usgrexmpl2.g ⊢ G = V E
4 1 2 3 usgrexmpl2nb0 ⊢ G NeighbVtx 0 = 1 3 5
5 4 eleq2i ⊢ b ∈ G NeighbVtx 0 ↔ b ∈ 1 3 5
6 vex ⊢ b ∈ V
7 6 eltp ⊢ b ∈ 1 3 5 ↔ b = 1 ∨ b = 3 ∨ b = 5
8 5 7 bitri ⊢ b ∈ G NeighbVtx 0 ↔ b = 1 ∨ b = 3 ∨ b = 5
9 4 eleq2i ⊢ c ∈ G NeighbVtx 0 ↔ c ∈ 1 3 5
10 vex ⊢ c ∈ V
11 10 eltp ⊢ c ∈ 1 3 5 ↔ c = 1 ∨ c = 3 ∨ c = 5
12 9 11 bitri ⊢ c ∈ G NeighbVtx 0 ↔ c = 1 ∨ c = 3 ∨ c = 5
13 eqtr3 ⊢ b = 1 ∧ c = 1 → b = c
14 13 orcd ⊢ b = 1 ∧ c = 1 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
15 ax-1ne0 ⊢ 1 ≠ 0
16 neeq1 ⊢ b = 1 → b ≠ 0 ↔ 1 ≠ 0
17 15 16 mpbiri ⊢ b = 1 → b ≠ 0
18 17 adantr ⊢ b = 1 ∧ c = 3 → b ≠ 0
19 18 neneqd ⊢ b = 1 ∧ c = 3 → ¬ b = 0
20 19 orcd ⊢ b = 1 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 3
21 3ne0 ⊢ 3 ≠ 0
22 neeq1 ⊢ c = 3 → c ≠ 0 ↔ 3 ≠ 0
23 21 22 mpbiri ⊢ c = 3 → c ≠ 0
24 23 adantl ⊢ b = 1 ∧ c = 3 → c ≠ 0
25 24 neneqd ⊢ b = 1 ∧ c = 3 → ¬ c = 0
26 25 olcd ⊢ b = 1 ∧ c = 3 → ¬ b = 3 ∨ ¬ c = 0
27 19 orcd ⊢ b = 1 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 1
28 25 olcd ⊢ b = 1 ∧ c = 3 → ¬ b = 1 ∨ ¬ c = 0
29 27 28 jca ⊢ b = 1 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
30 2re ⊢ 2 ∈ ℝ
31 2lt3 ⊢ 2 < 3
32 30 31 gtneii ⊢ 3 ≠ 2
33 neeq1 ⊢ c = 3 → c ≠ 2 ↔ 3 ≠ 2
34 32 33 mpbiri ⊢ c = 3 → c ≠ 2
35 34 adantl ⊢ b = 1 ∧ c = 3 → c ≠ 2
36 35 neneqd ⊢ b = 1 ∧ c = 3 → ¬ c = 2
37 36 olcd ⊢ b = 1 ∧ c = 3 → ¬ b = 1 ∨ ¬ c = 2
38 1re ⊢ 1 ∈ ℝ
39 1lt3 ⊢ 1 < 3
40 38 39 gtneii ⊢ 3 ≠ 1
41 neeq1 ⊢ c = 3 → c ≠ 1 ↔ 3 ≠ 1
42 40 41 mpbiri ⊢ c = 3 → c ≠ 1
43 42 adantl ⊢ b = 1 ∧ c = 3 → c ≠ 1
44 43 neneqd ⊢ b = 1 ∧ c = 3 → ¬ c = 1
45 44 olcd ⊢ b = 1 ∧ c = 3 → ¬ b = 2 ∨ ¬ c = 1
46 37 45 jca ⊢ b = 1 ∧ c = 3 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
47 1ne2 ⊢ 1 ≠ 2
48 neeq1 ⊢ b = 1 → b ≠ 2 ↔ 1 ≠ 2
49 47 48 mpbiri ⊢ b = 1 → b ≠ 2
50 49 adantr ⊢ b = 1 ∧ c = 3 → b ≠ 2
51 50 neneqd ⊢ b = 1 ∧ c = 3 → ¬ b = 2
52 51 orcd ⊢ b = 1 ∧ c = 3 → ¬ b = 2 ∨ ¬ c = 3
53 36 olcd ⊢ b = 1 ∧ c = 3 → ¬ b = 3 ∨ ¬ c = 2
54 52 53 jca ⊢ b = 1 ∧ c = 3 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
55 29 46 54 3jca ⊢ b = 1 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
56 38 39 ltneii ⊢ 1 ≠ 3
57 neeq1 ⊢ b = 1 → b ≠ 3 ↔ 1 ≠ 3
58 56 57 mpbiri ⊢ b = 1 → b ≠ 3
59 58 adantr ⊢ b = 1 ∧ c = 3 → b ≠ 3
60 59 neneqd ⊢ b = 1 ∧ c = 3 → ¬ b = 3
61 60 orcd ⊢ b = 1 ∧ c = 3 → ¬ b = 3 ∨ ¬ c = 4
62 1lt4 ⊢ 1 < 4
63 38 62 ltneii ⊢ 1 ≠ 4
64 neeq1 ⊢ b = 1 → b ≠ 4 ↔ 1 ≠ 4
65 63 64 mpbiri ⊢ b = 1 → b ≠ 4
66 65 adantr ⊢ b = 1 ∧ c = 3 → b ≠ 4
67 66 neneqd ⊢ b = 1 ∧ c = 3 → ¬ b = 4
68 67 orcd ⊢ b = 1 ∧ c = 3 → ¬ b = 4 ∨ ¬ c = 3
69 61 68 jca ⊢ b = 1 ∧ c = 3 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
70 67 orcd ⊢ b = 1 ∧ c = 3 → ¬ b = 4 ∨ ¬ c = 5
71 1lt5 ⊢ 1 < 5
72 38 71 ltneii ⊢ 1 ≠ 5
73 neeq1 ⊢ b = 1 → b ≠ 5 ↔ 1 ≠ 5
74 72 73 mpbiri ⊢ b = 1 → b ≠ 5
75 74 adantr ⊢ b = 1 ∧ c = 3 → b ≠ 5
76 75 neneqd ⊢ b = 1 ∧ c = 3 → ¬ b = 5
77 76 orcd ⊢ b = 1 ∧ c = 3 → ¬ b = 5 ∨ ¬ c = 4
78 70 77 jca ⊢ b = 1 ∧ c = 3 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
79 19 orcd ⊢ b = 1 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 5
80 25 olcd ⊢ b = 1 ∧ c = 3 → ¬ b = 5 ∨ ¬ c = 0
81 79 80 jca ⊢ b = 1 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
82 69 78 81 3jca ⊢ b = 1 ∧ c = 3 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
83 55 82 jca ⊢ b = 1 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
84 20 26 83 jca31 ⊢ b = 1 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
85 84 olcd ⊢ b = 1 ∧ c = 3 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
86 17 adantr ⊢ b = 1 ∧ c = 5 → b ≠ 0
87 86 neneqd ⊢ b = 1 ∧ c = 5 → ¬ b = 0
88 87 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 3
89 58 adantr ⊢ b = 1 ∧ c = 5 → b ≠ 3
90 89 neneqd ⊢ b = 1 ∧ c = 5 → ¬ b = 3
91 90 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 3 ∨ ¬ c = 0
92 87 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 1
93 0re ⊢ 0 ∈ ℝ
94 5pos ⊢ 0 < 5
95 93 94 gtneii ⊢ 5 ≠ 0
96 neeq1 ⊢ c = 5 → c ≠ 0 ↔ 5 ≠ 0
97 95 96 mpbiri ⊢ c = 5 → c ≠ 0
98 97 adantl ⊢ b = 1 ∧ c = 5 → c ≠ 0
99 98 neneqd ⊢ b = 1 ∧ c = 5 → ¬ c = 0
100 99 olcd ⊢ b = 1 ∧ c = 5 → ¬ b = 1 ∨ ¬ c = 0
101 92 100 jca ⊢ b = 1 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
102 2lt5 ⊢ 2 < 5
103 30 102 gtneii ⊢ 5 ≠ 2
104 neeq1 ⊢ c = 5 → c ≠ 2 ↔ 5 ≠ 2
105 103 104 mpbiri ⊢ c = 5 → c ≠ 2
106 105 adantl ⊢ b = 1 ∧ c = 5 → c ≠ 2
107 106 neneqd ⊢ b = 1 ∧ c = 5 → ¬ c = 2
108 107 olcd ⊢ b = 1 ∧ c = 5 → ¬ b = 1 ∨ ¬ c = 2
109 49 adantr ⊢ b = 1 ∧ c = 5 → b ≠ 2
110 109 neneqd ⊢ b = 1 ∧ c = 5 → ¬ b = 2
111 110 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 2 ∨ ¬ c = 1
112 108 111 jca ⊢ b = 1 ∧ c = 5 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
113 110 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 2 ∨ ¬ c = 3
114 90 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 3 ∨ ¬ c = 2
115 113 114 jca ⊢ b = 1 ∧ c = 5 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
116 101 112 115 3jca ⊢ b = 1 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
117 90 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 3 ∨ ¬ c = 4
118 65 adantr ⊢ b = 1 ∧ c = 5 → b ≠ 4
119 118 neneqd ⊢ b = 1 ∧ c = 5 → ¬ b = 4
120 119 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 4 ∨ ¬ c = 3
121 117 120 jca ⊢ b = 1 ∧ c = 5 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
122 119 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 4 ∨ ¬ c = 5
123 74 adantr ⊢ b = 1 ∧ c = 5 → b ≠ 5
124 123 neneqd ⊢ b = 1 ∧ c = 5 → ¬ b = 5
125 124 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 5 ∨ ¬ c = 4
126 122 125 jca ⊢ b = 1 ∧ c = 5 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
127 87 orcd ⊢ b = 1 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 5
128 99 olcd ⊢ b = 1 ∧ c = 5 → ¬ b = 5 ∨ ¬ c = 0
129 127 128 jca ⊢ b = 1 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
130 121 126 129 3jca ⊢ b = 1 ∧ c = 5 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
131 116 130 jca ⊢ b = 1 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
132 88 91 131 jca31 ⊢ b = 1 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
133 132 olcd ⊢ b = 1 ∧ c = 5 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
134 14 85 133 3jaodan ⊢ b = 1 ∧ c = 1 ∨ c = 3 ∨ c = 5 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
135 neeq1 ⊢ b = 3 → b ≠ 0 ↔ 3 ≠ 0
136 21 135 mpbiri ⊢ b = 3 → b ≠ 0
137 136 adantr ⊢ b = 3 ∧ c = 1 → b ≠ 0
138 137 neneqd ⊢ b = 3 ∧ c = 1 → ¬ b = 0
139 138 orcd ⊢ b = 3 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 3
140 neeq1 ⊢ c = 1 → c ≠ 0 ↔ 1 ≠ 0
141 15 140 mpbiri ⊢ c = 1 → c ≠ 0
142 141 adantl ⊢ b = 3 ∧ c = 1 → c ≠ 0
143 142 neneqd ⊢ b = 3 ∧ c = 1 → ¬ c = 0
144 143 olcd ⊢ b = 3 ∧ c = 1 → ¬ b = 3 ∨ ¬ c = 0
145 138 orcd ⊢ b = 3 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 1
146 143 olcd ⊢ b = 3 ∧ c = 1 → ¬ b = 1 ∨ ¬ c = 0
147 145 146 jca ⊢ b = 3 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
148 58 necon2i ⊢ b = 3 → b ≠ 1
149 148 adantr ⊢ b = 3 ∧ c = 1 → b ≠ 1
150 149 neneqd ⊢ b = 3 ∧ c = 1 → ¬ b = 1
151 150 orcd ⊢ b = 3 ∧ c = 1 → ¬ b = 1 ∨ ¬ c = 2
152 neeq1 ⊢ b = 3 → b ≠ 2 ↔ 3 ≠ 2
153 32 152 mpbiri ⊢ b = 3 → b ≠ 2
154 153 adantr ⊢ b = 3 ∧ c = 1 → b ≠ 2
155 154 neneqd ⊢ b = 3 ∧ c = 1 → ¬ b = 2
156 155 orcd ⊢ b = 3 ∧ c = 1 → ¬ b = 2 ∨ ¬ c = 1
157 151 156 jca ⊢ b = 3 ∧ c = 1 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
158 155 orcd ⊢ b = 3 ∧ c = 1 → ¬ b = 2 ∨ ¬ c = 3
159 neeq1 ⊢ c = 1 → c ≠ 2 ↔ 1 ≠ 2
160 47 159 mpbiri ⊢ c = 1 → c ≠ 2
161 160 adantl ⊢ b = 3 ∧ c = 1 → c ≠ 2
162 161 neneqd ⊢ b = 3 ∧ c = 1 → ¬ c = 2
163 162 olcd ⊢ b = 3 ∧ c = 1 → ¬ b = 3 ∨ ¬ c = 2
164 158 163 jca ⊢ b = 3 ∧ c = 1 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
165 147 157 164 3jca ⊢ b = 3 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
166 neeq1 ⊢ c = 1 → c ≠ 4 ↔ 1 ≠ 4
167 63 166 mpbiri ⊢ c = 1 → c ≠ 4
168 167 adantl ⊢ b = 3 ∧ c = 1 → c ≠ 4
169 168 neneqd ⊢ b = 3 ∧ c = 1 → ¬ c = 4
170 169 olcd ⊢ b = 3 ∧ c = 1 → ¬ b = 3 ∨ ¬ c = 4
171 42 necon2i ⊢ c = 1 → c ≠ 3
172 171 adantl ⊢ b = 3 ∧ c = 1 → c ≠ 3
173 172 neneqd ⊢ b = 3 ∧ c = 1 → ¬ c = 3
174 173 olcd ⊢ b = 3 ∧ c = 1 → ¬ b = 4 ∨ ¬ c = 3
175 170 174 jca ⊢ b = 3 ∧ c = 1 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
176 neeq1 ⊢ c = 1 → c ≠ 5 ↔ 1 ≠ 5
177 72 176 mpbiri ⊢ c = 1 → c ≠ 5
178 177 adantl ⊢ b = 3 ∧ c = 1 → c ≠ 5
179 178 neneqd ⊢ b = 3 ∧ c = 1 → ¬ c = 5
180 179 olcd ⊢ b = 3 ∧ c = 1 → ¬ b = 4 ∨ ¬ c = 5
181 169 olcd ⊢ b = 3 ∧ c = 1 → ¬ b = 5 ∨ ¬ c = 4
182 180 181 jca ⊢ b = 3 ∧ c = 1 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
183 138 orcd ⊢ b = 3 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 5
184 143 olcd ⊢ b = 3 ∧ c = 1 → ¬ b = 5 ∨ ¬ c = 0
185 183 184 jca ⊢ b = 3 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
186 175 182 185 3jca ⊢ b = 3 ∧ c = 1 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
187 165 186 jca ⊢ b = 3 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
188 139 144 187 jca31 ⊢ b = 3 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
189 188 olcd ⊢ b = 3 ∧ c = 1 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
190 eqtr3 ⊢ b = 3 ∧ c = 3 → b = c
191 190 orcd ⊢ b = 3 ∧ c = 3 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
192 136 adantr ⊢ b = 3 ∧ c = 5 → b ≠ 0
193 192 neneqd ⊢ b = 3 ∧ c = 5 → ¬ b = 0
194 193 orcd ⊢ b = 3 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 3
195 97 adantl ⊢ b = 3 ∧ c = 5 → c ≠ 0
196 195 neneqd ⊢ b = 3 ∧ c = 5 → ¬ c = 0
197 196 olcd ⊢ b = 3 ∧ c = 5 → ¬ b = 3 ∨ ¬ c = 0
198 193 orcd ⊢ b = 3 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 1
199 196 olcd ⊢ b = 3 ∧ c = 5 → ¬ b = 1 ∨ ¬ c = 0
200 198 199 jca ⊢ b = 3 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
201 148 adantr ⊢ b = 3 ∧ c = 5 → b ≠ 1
202 201 neneqd ⊢ b = 3 ∧ c = 5 → ¬ b = 1
203 202 orcd ⊢ b = 3 ∧ c = 5 → ¬ b = 1 ∨ ¬ c = 2
204 177 necon2i ⊢ c = 5 → c ≠ 1
205 204 adantl ⊢ b = 3 ∧ c = 5 → c ≠ 1
206 205 neneqd ⊢ b = 3 ∧ c = 5 → ¬ c = 1
207 206 olcd ⊢ b = 3 ∧ c = 5 → ¬ b = 2 ∨ ¬ c = 1
208 203 207 jca ⊢ b = 3 ∧ c = 5 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
209 153 adantr ⊢ b = 3 ∧ c = 5 → b ≠ 2
210 209 neneqd ⊢ b = 3 ∧ c = 5 → ¬ b = 2
211 210 orcd ⊢ b = 3 ∧ c = 5 → ¬ b = 2 ∨ ¬ c = 3
212 105 adantl ⊢ b = 3 ∧ c = 5 → c ≠ 2
213 212 neneqd ⊢ b = 3 ∧ c = 5 → ¬ c = 2
214 213 olcd ⊢ b = 3 ∧ c = 5 → ¬ b = 3 ∨ ¬ c = 2
215 211 214 jca ⊢ b = 3 ∧ c = 5 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
216 200 208 215 3jca ⊢ b = 3 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
217 4re ⊢ 4 ∈ ℝ
218 4lt5 ⊢ 4 < 5
219 217 218 gtneii ⊢ 5 ≠ 4
220 neeq1 ⊢ c = 5 → c ≠ 4 ↔ 5 ≠ 4
221 219 220 mpbiri ⊢ c = 5 → c ≠ 4
222 221 adantl ⊢ b = 3 ∧ c = 5 → c ≠ 4
223 222 neneqd ⊢ b = 3 ∧ c = 5 → ¬ c = 4
224 223 olcd ⊢ b = 3 ∧ c = 5 → ¬ b = 3 ∨ ¬ c = 4
225 3re ⊢ 3 ∈ ℝ
226 3lt4 ⊢ 3 < 4
227 225 226 ltneii ⊢ 3 ≠ 4
228 neeq1 ⊢ b = 3 → b ≠ 4 ↔ 3 ≠ 4
229 227 228 mpbiri ⊢ b = 3 → b ≠ 4
230 229 adantr ⊢ b = 3 ∧ c = 5 → b ≠ 4
231 230 neneqd ⊢ b = 3 ∧ c = 5 → ¬ b = 4
232 231 orcd ⊢ b = 3 ∧ c = 5 → ¬ b = 4 ∨ ¬ c = 3
233 224 232 jca ⊢ b = 3 ∧ c = 5 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
234 231 orcd ⊢ b = 3 ∧ c = 5 → ¬ b = 4 ∨ ¬ c = 5
235 223 olcd ⊢ b = 3 ∧ c = 5 → ¬ b = 5 ∨ ¬ c = 4
236 234 235 jca ⊢ b = 3 ∧ c = 5 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
237 193 orcd ⊢ b = 3 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 5
238 196 olcd ⊢ b = 3 ∧ c = 5 → ¬ b = 5 ∨ ¬ c = 0
239 237 238 jca ⊢ b = 3 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
240 233 236 239 3jca ⊢ b = 3 ∧ c = 5 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
241 216 240 jca ⊢ b = 3 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
242 194 197 241 jca31 ⊢ b = 3 ∧ c = 5 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
243 242 olcd ⊢ b = 3 ∧ c = 5 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
244 189 191 243 3jaodan ⊢ b = 3 ∧ c = 1 ∨ c = 3 ∨ c = 5 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
245 171 adantl ⊢ b = 5 ∧ c = 1 → c ≠ 3
246 245 neneqd ⊢ b = 5 ∧ c = 1 → ¬ c = 3
247 246 olcd ⊢ b = 5 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 3
248 141 adantl ⊢ b = 5 ∧ c = 1 → c ≠ 0
249 248 neneqd ⊢ b = 5 ∧ c = 1 → ¬ c = 0
250 249 olcd ⊢ b = 5 ∧ c = 1 → ¬ b = 3 ∨ ¬ c = 0
251 neeq1 ⊢ b = 5 → b ≠ 0 ↔ 5 ≠ 0
252 95 251 mpbiri ⊢ b = 5 → b ≠ 0
253 252 adantr ⊢ b = 5 ∧ c = 1 → b ≠ 0
254 253 neneqd ⊢ b = 5 ∧ c = 1 → ¬ b = 0
255 254 orcd ⊢ b = 5 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 1
256 249 olcd ⊢ b = 5 ∧ c = 1 → ¬ b = 1 ∨ ¬ c = 0
257 255 256 jca ⊢ b = 5 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
258 74 necon2i ⊢ b = 5 → b ≠ 1
259 258 adantr ⊢ b = 5 ∧ c = 1 → b ≠ 1
260 259 neneqd ⊢ b = 5 ∧ c = 1 → ¬ b = 1
261 260 orcd ⊢ b = 5 ∧ c = 1 → ¬ b = 1 ∨ ¬ c = 2
262 neeq1 ⊢ b = 5 → b ≠ 2 ↔ 5 ≠ 2
263 103 262 mpbiri ⊢ b = 5 → b ≠ 2
264 263 adantr ⊢ b = 5 ∧ c = 1 → b ≠ 2
265 264 neneqd ⊢ b = 5 ∧ c = 1 → ¬ b = 2
266 265 orcd ⊢ b = 5 ∧ c = 1 → ¬ b = 2 ∨ ¬ c = 1
267 261 266 jca ⊢ b = 5 ∧ c = 1 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
268 246 olcd ⊢ b = 5 ∧ c = 1 → ¬ b = 2 ∨ ¬ c = 3
269 160 adantl ⊢ b = 5 ∧ c = 1 → c ≠ 2
270 269 neneqd ⊢ b = 5 ∧ c = 1 → ¬ c = 2
271 270 olcd ⊢ b = 5 ∧ c = 1 → ¬ b = 3 ∨ ¬ c = 2
272 268 271 jca ⊢ b = 5 ∧ c = 1 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
273 257 267 272 3jca ⊢ b = 5 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
274 3lt5 ⊢ 3 < 5
275 225 274 gtneii ⊢ 5 ≠ 3
276 neeq1 ⊢ b = 5 → b ≠ 3 ↔ 5 ≠ 3
277 275 276 mpbiri ⊢ b = 5 → b ≠ 3
278 277 adantr ⊢ b = 5 ∧ c = 1 → b ≠ 3
279 278 neneqd ⊢ b = 5 ∧ c = 1 → ¬ b = 3
280 279 orcd ⊢ b = 5 ∧ c = 1 → ¬ b = 3 ∨ ¬ c = 4
281 246 olcd ⊢ b = 5 ∧ c = 1 → ¬ b = 4 ∨ ¬ c = 3
282 280 281 jca ⊢ b = 5 ∧ c = 1 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
283 177 adantl ⊢ b = 5 ∧ c = 1 → c ≠ 5
284 283 neneqd ⊢ b = 5 ∧ c = 1 → ¬ c = 5
285 284 olcd ⊢ b = 5 ∧ c = 1 → ¬ b = 4 ∨ ¬ c = 5
286 167 adantl ⊢ b = 5 ∧ c = 1 → c ≠ 4
287 286 neneqd ⊢ b = 5 ∧ c = 1 → ¬ c = 4
288 287 olcd ⊢ b = 5 ∧ c = 1 → ¬ b = 5 ∨ ¬ c = 4
289 285 288 jca ⊢ b = 5 ∧ c = 1 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
290 254 orcd ⊢ b = 5 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 5
291 249 olcd ⊢ b = 5 ∧ c = 1 → ¬ b = 5 ∨ ¬ c = 0
292 290 291 jca ⊢ b = 5 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
293 282 289 292 3jca ⊢ b = 5 ∧ c = 1 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
294 273 293 jca ⊢ b = 5 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
295 247 250 294 jca31 ⊢ b = 5 ∧ c = 1 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
296 295 olcd ⊢ b = 5 ∧ c = 1 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
297 252 adantr ⊢ b = 5 ∧ c = 3 → b ≠ 0
298 297 neneqd ⊢ b = 5 ∧ c = 3 → ¬ b = 0
299 298 orcd ⊢ b = 5 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 3
300 23 adantl ⊢ b = 5 ∧ c = 3 → c ≠ 0
301 300 neneqd ⊢ b = 5 ∧ c = 3 → ¬ c = 0
302 301 olcd ⊢ b = 5 ∧ c = 3 → ¬ b = 3 ∨ ¬ c = 0
303 298 orcd ⊢ b = 5 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 1
304 301 olcd ⊢ b = 5 ∧ c = 3 → ¬ b = 1 ∨ ¬ c = 0
305 303 304 jca ⊢ b = 5 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
306 258 adantr ⊢ b = 5 ∧ c = 3 → b ≠ 1
307 306 neneqd ⊢ b = 5 ∧ c = 3 → ¬ b = 1
308 307 orcd ⊢ b = 5 ∧ c = 3 → ¬ b = 1 ∨ ¬ c = 2
309 42 adantl ⊢ b = 5 ∧ c = 3 → c ≠ 1
310 309 neneqd ⊢ b = 5 ∧ c = 3 → ¬ c = 1
311 310 olcd ⊢ b = 5 ∧ c = 3 → ¬ b = 2 ∨ ¬ c = 1
312 308 311 jca ⊢ b = 5 ∧ c = 3 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
313 263 adantr ⊢ b = 5 ∧ c = 3 → b ≠ 2
314 313 neneqd ⊢ b = 5 ∧ c = 3 → ¬ b = 2
315 314 orcd ⊢ b = 5 ∧ c = 3 → ¬ b = 2 ∨ ¬ c = 3
316 277 adantr ⊢ b = 5 ∧ c = 3 → b ≠ 3
317 316 neneqd ⊢ b = 5 ∧ c = 3 → ¬ b = 3
318 317 orcd ⊢ b = 5 ∧ c = 3 → ¬ b = 3 ∨ ¬ c = 2
319 315 318 jca ⊢ b = 5 ∧ c = 3 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
320 305 312 319 3jca ⊢ b = 5 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
321 317 orcd ⊢ b = 5 ∧ c = 3 → ¬ b = 3 ∨ ¬ c = 4
322 neeq1 ⊢ b = 5 → b ≠ 4 ↔ 5 ≠ 4
323 219 322 mpbiri ⊢ b = 5 → b ≠ 4
324 323 adantr ⊢ b = 5 ∧ c = 3 → b ≠ 4
325 324 neneqd ⊢ b = 5 ∧ c = 3 → ¬ b = 4
326 325 orcd ⊢ b = 5 ∧ c = 3 → ¬ b = 4 ∨ ¬ c = 3
327 321 326 jca ⊢ b = 5 ∧ c = 3 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
328 325 orcd ⊢ b = 5 ∧ c = 3 → ¬ b = 4 ∨ ¬ c = 5
329 neeq1 ⊢ c = 3 → c ≠ 4 ↔ 3 ≠ 4
330 227 329 mpbiri ⊢ c = 3 → c ≠ 4
331 330 adantl ⊢ b = 5 ∧ c = 3 → c ≠ 4
332 331 neneqd ⊢ b = 5 ∧ c = 3 → ¬ c = 4
333 332 olcd ⊢ b = 5 ∧ c = 3 → ¬ b = 5 ∨ ¬ c = 4
334 328 333 jca ⊢ b = 5 ∧ c = 3 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
335 298 orcd ⊢ b = 5 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 5
336 301 olcd ⊢ b = 5 ∧ c = 3 → ¬ b = 5 ∨ ¬ c = 0
337 335 336 jca ⊢ b = 5 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
338 327 334 337 3jca ⊢ b = 5 ∧ c = 3 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
339 320 338 jca ⊢ b = 5 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
340 299 302 339 jca31 ⊢ b = 5 ∧ c = 3 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
341 340 olcd ⊢ b = 5 ∧ c = 3 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
342 eqtr3 ⊢ b = 5 ∧ c = 5 → b = c
343 342 orcd ⊢ b = 5 ∧ c = 5 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
344 296 341 343 3jaodan ⊢ b = 5 ∧ c = 1 ∨ c = 3 ∨ c = 5 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
345 134 244 344 3jaoian ⊢ b = 1 ∨ b = 3 ∨ b = 5 ∧ c = 1 ∨ c = 3 ∨ c = 5 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
346 8 12 345 syl2anb ⊢ b ∈ G NeighbVtx 0 ∧ c ∈ G NeighbVtx 0 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
347 346 rgen2 ⊢ ∀ b ∈ G NeighbVtx 0 ∀ c ∈ G NeighbVtx 0 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
348 1 2 3 usgrexmpl2nb1 ⊢ G NeighbVtx 1 = 0 2
349 348 eleq2i ⊢ b ∈ G NeighbVtx 1 ↔ b ∈ 0 2
350 6 elpr ⊢ b ∈ 0 2 ↔ b = 0 ∨ b = 2
351 349 350 bitri ⊢ b ∈ G NeighbVtx 1 ↔ b = 0 ∨ b = 2
352 348 eleq2i ⊢ c ∈ G NeighbVtx 1 ↔ c ∈ 0 2
353 10 elpr ⊢ c ∈ 0 2 ↔ c = 0 ∨ c = 2
354 352 353 bitri ⊢ c ∈ G NeighbVtx 1 ↔ c = 0 ∨ c = 2
355 eqtr3 ⊢ b = 0 ∧ c = 0 → b = c
356 355 orcd ⊢ b = 0 ∧ c = 0 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
357 2ne0 ⊢ 2 ≠ 0
358 neeq1 ⊢ b = 2 → b ≠ 0 ↔ 2 ≠ 0
359 357 358 mpbiri ⊢ b = 2 → b ≠ 0
360 359 adantr ⊢ b = 2 ∧ c = 0 → b ≠ 0
361 360 neneqd ⊢ b = 2 ∧ c = 0 → ¬ b = 0
362 361 orcd ⊢ b = 2 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 3
363 153 necon2i ⊢ b = 2 → b ≠ 3
364 363 adantr ⊢ b = 2 ∧ c = 0 → b ≠ 3
365 364 neneqd ⊢ b = 2 ∧ c = 0 → ¬ b = 3
366 365 orcd ⊢ b = 2 ∧ c = 0 → ¬ b = 3 ∨ ¬ c = 0
367 361 orcd ⊢ b = 2 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 1
368 49 necon2i ⊢ b = 2 → b ≠ 1
369 368 adantr ⊢ b = 2 ∧ c = 0 → b ≠ 1
370 369 neneqd ⊢ b = 2 ∧ c = 0 → ¬ b = 1
371 370 orcd ⊢ b = 2 ∧ c = 0 → ¬ b = 1 ∨ ¬ c = 0
372 367 371 jca ⊢ b = 2 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
373 370 orcd ⊢ b = 2 ∧ c = 0 → ¬ b = 1 ∨ ¬ c = 2
374 141 necon2i ⊢ c = 0 → c ≠ 1
375 374 adantl ⊢ b = 2 ∧ c = 0 → c ≠ 1
376 375 neneqd ⊢ b = 2 ∧ c = 0 → ¬ c = 1
377 376 olcd ⊢ b = 2 ∧ c = 0 → ¬ b = 2 ∨ ¬ c = 1
378 373 377 jca ⊢ b = 2 ∧ c = 0 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
379 23 necon2i ⊢ c = 0 → c ≠ 3
380 379 adantl ⊢ b = 2 ∧ c = 0 → c ≠ 3
381 380 neneqd ⊢ b = 2 ∧ c = 0 → ¬ c = 3
382 381 olcd ⊢ b = 2 ∧ c = 0 → ¬ b = 2 ∨ ¬ c = 3
383 365 orcd ⊢ b = 2 ∧ c = 0 → ¬ b = 3 ∨ ¬ c = 2
384 382 383 jca ⊢ b = 2 ∧ c = 0 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
385 372 378 384 3jca ⊢ b = 2 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
386 365 orcd ⊢ b = 2 ∧ c = 0 → ¬ b = 3 ∨ ¬ c = 4
387 381 olcd ⊢ b = 2 ∧ c = 0 → ¬ b = 4 ∨ ¬ c = 3
388 386 387 jca ⊢ b = 2 ∧ c = 0 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
389 97 necon2i ⊢ c = 0 → c ≠ 5
390 389 adantl ⊢ b = 2 ∧ c = 0 → c ≠ 5
391 390 neneqd ⊢ b = 2 ∧ c = 0 → ¬ c = 5
392 391 olcd ⊢ b = 2 ∧ c = 0 → ¬ b = 4 ∨ ¬ c = 5
393 4pos ⊢ 0 < 4
394 93 393 ltneii ⊢ 0 ≠ 4
395 neeq1 ⊢ c = 0 → c ≠ 4 ↔ 0 ≠ 4
396 394 395 mpbiri ⊢ c = 0 → c ≠ 4
397 396 adantl ⊢ b = 2 ∧ c = 0 → c ≠ 4
398 397 neneqd ⊢ b = 2 ∧ c = 0 → ¬ c = 4
399 398 olcd ⊢ b = 2 ∧ c = 0 → ¬ b = 5 ∨ ¬ c = 4
400 392 399 jca ⊢ b = 2 ∧ c = 0 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
401 361 orcd ⊢ b = 2 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 5
402 263 necon2i ⊢ b = 2 → b ≠ 5
403 402 adantr ⊢ b = 2 ∧ c = 0 → b ≠ 5
404 403 neneqd ⊢ b = 2 ∧ c = 0 → ¬ b = 5
405 404 orcd ⊢ b = 2 ∧ c = 0 → ¬ b = 5 ∨ ¬ c = 0
406 401 405 jca ⊢ b = 2 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
407 388 400 406 3jca ⊢ b = 2 ∧ c = 0 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
408 385 407 jca ⊢ b = 2 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
409 362 366 408 jca31 ⊢ b = 2 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
410 409 olcd ⊢ b = 2 ∧ c = 0 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
411 34 necon2i ⊢ c = 2 → c ≠ 3
412 411 adantl ⊢ b = 0 ∧ c = 2 → c ≠ 3
413 412 neneqd ⊢ b = 0 ∧ c = 2 → ¬ c = 3
414 413 olcd ⊢ b = 0 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 3
415 neeq1 ⊢ c = 2 → c ≠ 0 ↔ 2 ≠ 0
416 357 415 mpbiri ⊢ c = 2 → c ≠ 0
417 416 adantl ⊢ b = 0 ∧ c = 2 → c ≠ 0
418 417 neneqd ⊢ b = 0 ∧ c = 2 → ¬ c = 0
419 418 olcd ⊢ b = 0 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 0
420 160 necon2i ⊢ c = 2 → c ≠ 1
421 420 adantl ⊢ b = 0 ∧ c = 2 → c ≠ 1
422 421 neneqd ⊢ b = 0 ∧ c = 2 → ¬ c = 1
423 422 olcd ⊢ b = 0 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1
424 418 olcd ⊢ b = 0 ∧ c = 2 → ¬ b = 1 ∨ ¬ c = 0
425 423 424 jca ⊢ b = 0 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
426 17 necon2i ⊢ b = 0 → b ≠ 1
427 426 adantr ⊢ b = 0 ∧ c = 2 → b ≠ 1
428 427 neneqd ⊢ b = 0 ∧ c = 2 → ¬ b = 1
429 428 orcd ⊢ b = 0 ∧ c = 2 → ¬ b = 1 ∨ ¬ c = 2
430 359 necon2i ⊢ b = 0 → b ≠ 2
431 430 adantr ⊢ b = 0 ∧ c = 2 → b ≠ 2
432 431 neneqd ⊢ b = 0 ∧ c = 2 → ¬ b = 2
433 432 orcd ⊢ b = 0 ∧ c = 2 → ¬ b = 2 ∨ ¬ c = 1
434 429 433 jca ⊢ b = 0 ∧ c = 2 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
435 413 olcd ⊢ b = 0 ∧ c = 2 → ¬ b = 2 ∨ ¬ c = 3
436 136 necon2i ⊢ b = 0 → b ≠ 3
437 436 adantr ⊢ b = 0 ∧ c = 2 → b ≠ 3
438 437 neneqd ⊢ b = 0 ∧ c = 2 → ¬ b = 3
439 438 orcd ⊢ b = 0 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 2
440 435 439 jca ⊢ b = 0 ∧ c = 2 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
441 425 434 440 3jca ⊢ b = 0 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
442 438 orcd ⊢ b = 0 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 4
443 413 olcd ⊢ b = 0 ∧ c = 2 → ¬ b = 4 ∨ ¬ c = 3
444 442 443 jca ⊢ b = 0 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
445 neeq1 ⊢ b = 0 → b ≠ 4 ↔ 0 ≠ 4
446 394 445 mpbiri ⊢ b = 0 → b ≠ 4
447 446 adantr ⊢ b = 0 ∧ c = 2 → b ≠ 4
448 447 neneqd ⊢ b = 0 ∧ c = 2 → ¬ b = 4
449 448 orcd ⊢ b = 0 ∧ c = 2 → ¬ b = 4 ∨ ¬ c = 5
450 252 necon2i ⊢ b = 0 → b ≠ 5
451 450 adantr ⊢ b = 0 ∧ c = 2 → b ≠ 5
452 451 neneqd ⊢ b = 0 ∧ c = 2 → ¬ b = 5
453 452 orcd ⊢ b = 0 ∧ c = 2 → ¬ b = 5 ∨ ¬ c = 4
454 449 453 jca ⊢ b = 0 ∧ c = 2 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
455 105 necon2i ⊢ c = 2 → c ≠ 5
456 455 adantl ⊢ b = 0 ∧ c = 2 → c ≠ 5
457 456 neneqd ⊢ b = 0 ∧ c = 2 → ¬ c = 5
458 457 olcd ⊢ b = 0 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 5
459 418 olcd ⊢ b = 0 ∧ c = 2 → ¬ b = 5 ∨ ¬ c = 0
460 458 459 jca ⊢ b = 0 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
461 444 454 460 3jca ⊢ b = 0 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
462 441 461 jca ⊢ b = 0 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
463 414 419 462 jca31 ⊢ b = 0 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
464 463 olcd ⊢ b = 0 ∧ c = 2 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
465 359 adantr ⊢ b = 2 ∧ c = 2 → b ≠ 0
466 465 neneqd ⊢ b = 2 ∧ c = 2 → ¬ b = 0
467 466 orcd ⊢ b = 2 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 3
468 416 adantl ⊢ b = 2 ∧ c = 2 → c ≠ 0
469 468 neneqd ⊢ b = 2 ∧ c = 2 → ¬ c = 0
470 469 olcd ⊢ b = 2 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 0
471 466 orcd ⊢ b = 2 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1
472 469 olcd ⊢ b = 2 ∧ c = 2 → ¬ b = 1 ∨ ¬ c = 0
473 471 472 jca ⊢ b = 2 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
474 368 adantr ⊢ b = 2 ∧ c = 2 → b ≠ 1
475 474 neneqd ⊢ b = 2 ∧ c = 2 → ¬ b = 1
476 475 orcd ⊢ b = 2 ∧ c = 2 → ¬ b = 1 ∨ ¬ c = 2
477 420 adantl ⊢ b = 2 ∧ c = 2 → c ≠ 1
478 477 neneqd ⊢ b = 2 ∧ c = 2 → ¬ c = 1
479 478 olcd ⊢ b = 2 ∧ c = 2 → ¬ b = 2 ∨ ¬ c = 1
480 476 479 jca ⊢ b = 2 ∧ c = 2 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
481 411 adantl ⊢ b = 2 ∧ c = 2 → c ≠ 3
482 481 neneqd ⊢ b = 2 ∧ c = 2 → ¬ c = 3
483 482 olcd ⊢ b = 2 ∧ c = 2 → ¬ b = 2 ∨ ¬ c = 3
484 363 adantr ⊢ b = 2 ∧ c = 2 → b ≠ 3
485 484 neneqd ⊢ b = 2 ∧ c = 2 → ¬ b = 3
486 485 orcd ⊢ b = 2 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 2
487 483 486 jca ⊢ b = 2 ∧ c = 2 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
488 473 480 487 3jca ⊢ b = 2 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
489 485 orcd ⊢ b = 2 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 4
490 2lt4 ⊢ 2 < 4
491 30 490 ltneii ⊢ 2 ≠ 4
492 neeq1 ⊢ b = 2 → b ≠ 4 ↔ 2 ≠ 4
493 491 492 mpbiri ⊢ b = 2 → b ≠ 4
494 493 adantr ⊢ b = 2 ∧ c = 2 → b ≠ 4
495 494 neneqd ⊢ b = 2 ∧ c = 2 → ¬ b = 4
496 495 orcd ⊢ b = 2 ∧ c = 2 → ¬ b = 4 ∨ ¬ c = 3
497 489 496 jca ⊢ b = 2 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
498 495 orcd ⊢ b = 2 ∧ c = 2 → ¬ b = 4 ∨ ¬ c = 5
499 402 adantr ⊢ b = 2 ∧ c = 2 → b ≠ 5
500 499 neneqd ⊢ b = 2 ∧ c = 2 → ¬ b = 5
501 500 orcd ⊢ b = 2 ∧ c = 2 → ¬ b = 5 ∨ ¬ c = 4
502 498 501 jca ⊢ b = 2 ∧ c = 2 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
503 466 orcd ⊢ b = 2 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 5
504 469 olcd ⊢ b = 2 ∧ c = 2 → ¬ b = 5 ∨ ¬ c = 0
505 503 504 jca ⊢ b = 2 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
506 497 502 505 3jca ⊢ b = 2 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
507 488 506 jca ⊢ b = 2 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
508 467 470 507 jca31 ⊢ b = 2 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
509 508 olcd ⊢ b = 2 ∧ c = 2 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
510 356 410 464 509 ccase ⊢ b = 0 ∨ b = 2 ∧ c = 0 ∨ c = 2 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
511 351 354 510 syl2anb ⊢ b ∈ G NeighbVtx 1 ∧ c ∈ G NeighbVtx 1 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
512 511 rgen2 ⊢ ∀ b ∈ G NeighbVtx 1 ∀ c ∈ G NeighbVtx 1 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
513 1 2 3 usgrexmpl2nb2 ⊢ G NeighbVtx 2 = 1 3
514 513 eleq2i ⊢ b ∈ G NeighbVtx 2 ↔ b ∈ 1 3
515 6 elpr ⊢ b ∈ 1 3 ↔ b = 1 ∨ b = 3
516 514 515 bitri ⊢ b ∈ G NeighbVtx 2 ↔ b = 1 ∨ b = 3
517 513 eleq2i ⊢ c ∈ G NeighbVtx 2 ↔ c ∈ 1 3
518 10 elpr ⊢ c ∈ 1 3 ↔ c = 1 ∨ c = 3
519 517 518 bitri ⊢ c ∈ G NeighbVtx 2 ↔ c = 1 ∨ c = 3
520 14 189 85 191 ccase ⊢ b = 1 ∨ b = 3 ∧ c = 1 ∨ c = 3 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
521 516 519 520 syl2anb ⊢ b ∈ G NeighbVtx 2 ∧ c ∈ G NeighbVtx 2 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
522 521 rgen2 ⊢ ∀ b ∈ G NeighbVtx 2 ∀ c ∈ G NeighbVtx 2 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
523 c0ex ⊢ 0 ∈ V
524 1ex ⊢ 1 ∈ V
525 2ex ⊢ 2 ∈ V
526 oveq2 ⊢ a = 0 → G NeighbVtx a = G NeighbVtx 0
527 526 raleqdv ⊢ a = 0 → ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ c ∈ G NeighbVtx 0 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
528 526 527 raleqbidv ⊢ a = 0 → ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ b ∈ G NeighbVtx 0 ∀ c ∈ G NeighbVtx 0 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
529 oveq2 ⊢ a = 1 → G NeighbVtx a = G NeighbVtx 1
530 529 raleqdv ⊢ a = 1 → ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ c ∈ G NeighbVtx 1 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
531 529 530 raleqbidv ⊢ a = 1 → ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ b ∈ G NeighbVtx 1 ∀ c ∈ G NeighbVtx 1 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
532 oveq2 ⊢ a = 2 → G NeighbVtx a = G NeighbVtx 2
533 532 raleqdv ⊢ a = 2 → ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ c ∈ G NeighbVtx 2 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
534 532 533 raleqbidv ⊢ a = 2 → ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ b ∈ G NeighbVtx 2 ∀ c ∈ G NeighbVtx 2 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
535 523 524 525 528 531 534 raltp ⊢ ∀ a ∈ 0 1 2 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ b ∈ G NeighbVtx 0 ∀ c ∈ G NeighbVtx 0 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ∧ ∀ b ∈ G NeighbVtx 1 ∀ c ∈ G NeighbVtx 1 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ∧ ∀ b ∈ G NeighbVtx 2 ∀ c ∈ G NeighbVtx 2 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
536 347 512 522 535 mpbir3an ⊢ ∀ a ∈ 0 1 2 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
537 1 2 3 usgrexmpl2nb3 ⊢ G NeighbVtx 3 = 0 2 4
538 537 eleq2i ⊢ b ∈ G NeighbVtx 3 ↔ b ∈ 0 2 4
539 6 eltp ⊢ b ∈ 0 2 4 ↔ b = 0 ∨ b = 2 ∨ b = 4
540 538 539 bitri ⊢ b ∈ G NeighbVtx 3 ↔ b = 0 ∨ b = 2 ∨ b = 4
541 537 eleq2i ⊢ c ∈ G NeighbVtx 3 ↔ c ∈ 0 2 4
542 10 eltp ⊢ c ∈ 0 2 4 ↔ c = 0 ∨ c = 2 ∨ c = 4
543 541 542 bitri ⊢ c ∈ G NeighbVtx 3 ↔ c = 0 ∨ c = 2 ∨ c = 4
544 330 necon2i ⊢ c = 4 → c ≠ 3
545 544 adantl ⊢ b = 0 ∧ c = 4 → c ≠ 3
546 545 neneqd ⊢ b = 0 ∧ c = 4 → ¬ c = 3
547 546 olcd ⊢ b = 0 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 3
548 436 adantr ⊢ b = 0 ∧ c = 4 → b ≠ 3
549 548 neneqd ⊢ b = 0 ∧ c = 4 → ¬ b = 3
550 549 orcd ⊢ b = 0 ∧ c = 4 → ¬ b = 3 ∨ ¬ c = 0
551 167 necon2i ⊢ c = 4 → c ≠ 1
552 551 adantl ⊢ b = 0 ∧ c = 4 → c ≠ 1
553 552 neneqd ⊢ b = 0 ∧ c = 4 → ¬ c = 1
554 553 olcd ⊢ b = 0 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 1
555 426 adantr ⊢ b = 0 ∧ c = 4 → b ≠ 1
556 555 neneqd ⊢ b = 0 ∧ c = 4 → ¬ b = 1
557 556 orcd ⊢ b = 0 ∧ c = 4 → ¬ b = 1 ∨ ¬ c = 0
558 554 557 jca ⊢ b = 0 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
559 556 orcd ⊢ b = 0 ∧ c = 4 → ¬ b = 1 ∨ ¬ c = 2
560 430 adantr ⊢ b = 0 ∧ c = 4 → b ≠ 2
561 560 neneqd ⊢ b = 0 ∧ c = 4 → ¬ b = 2
562 561 orcd ⊢ b = 0 ∧ c = 4 → ¬ b = 2 ∨ ¬ c = 1
563 559 562 jca ⊢ b = 0 ∧ c = 4 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
564 546 olcd ⊢ b = 0 ∧ c = 4 → ¬ b = 2 ∨ ¬ c = 3
565 549 orcd ⊢ b = 0 ∧ c = 4 → ¬ b = 3 ∨ ¬ c = 2
566 564 565 jca ⊢ b = 0 ∧ c = 4 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
567 558 563 566 3jca ⊢ b = 0 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
568 549 orcd ⊢ b = 0 ∧ c = 4 → ¬ b = 3 ∨ ¬ c = 4
569 546 olcd ⊢ b = 0 ∧ c = 4 → ¬ b = 4 ∨ ¬ c = 3
570 568 569 jca ⊢ b = 0 ∧ c = 4 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
571 446 adantr ⊢ b = 0 ∧ c = 4 → b ≠ 4
572 571 neneqd ⊢ b = 0 ∧ c = 4 → ¬ b = 4
573 572 orcd ⊢ b = 0 ∧ c = 4 → ¬ b = 4 ∨ ¬ c = 5
574 450 adantr ⊢ b = 0 ∧ c = 4 → b ≠ 5
575 574 neneqd ⊢ b = 0 ∧ c = 4 → ¬ b = 5
576 575 orcd ⊢ b = 0 ∧ c = 4 → ¬ b = 5 ∨ ¬ c = 4
577 573 576 jca ⊢ b = 0 ∧ c = 4 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
578 221 necon2i ⊢ c = 4 → c ≠ 5
579 578 adantl ⊢ b = 0 ∧ c = 4 → c ≠ 5
580 579 neneqd ⊢ b = 0 ∧ c = 4 → ¬ c = 5
581 580 olcd ⊢ b = 0 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 5
582 396 necon2i ⊢ c = 4 → c ≠ 0
583 582 adantl ⊢ b = 0 ∧ c = 4 → c ≠ 0
584 583 neneqd ⊢ b = 0 ∧ c = 4 → ¬ c = 0
585 584 olcd ⊢ b = 0 ∧ c = 4 → ¬ b = 5 ∨ ¬ c = 0
586 581 585 jca ⊢ b = 0 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
587 570 577 586 3jca ⊢ b = 0 ∧ c = 4 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
588 567 587 jca ⊢ b = 0 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
589 547 550 588 jca31 ⊢ b = 0 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
590 589 olcd ⊢ b = 0 ∧ c = 4 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
591 356 464 590 3jaodan ⊢ b = 0 ∧ c = 0 ∨ c = 2 ∨ c = 4 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
592 359 adantr ⊢ b = 2 ∧ c = 4 → b ≠ 0
593 592 neneqd ⊢ b = 2 ∧ c = 4 → ¬ b = 0
594 593 orcd ⊢ b = 2 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 3
595 582 adantl ⊢ b = 2 ∧ c = 4 → c ≠ 0
596 595 neneqd ⊢ b = 2 ∧ c = 4 → ¬ c = 0
597 596 olcd ⊢ b = 2 ∧ c = 4 → ¬ b = 3 ∨ ¬ c = 0
598 593 orcd ⊢ b = 2 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 1
599 596 olcd ⊢ b = 2 ∧ c = 4 → ¬ b = 1 ∨ ¬ c = 0
600 598 599 jca ⊢ b = 2 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
601 368 adantr ⊢ b = 2 ∧ c = 4 → b ≠ 1
602 601 neneqd ⊢ b = 2 ∧ c = 4 → ¬ b = 1
603 602 orcd ⊢ b = 2 ∧ c = 4 → ¬ b = 1 ∨ ¬ c = 2
604 551 adantl ⊢ b = 2 ∧ c = 4 → c ≠ 1
605 604 neneqd ⊢ b = 2 ∧ c = 4 → ¬ c = 1
606 605 olcd ⊢ b = 2 ∧ c = 4 → ¬ b = 2 ∨ ¬ c = 1
607 603 606 jca ⊢ b = 2 ∧ c = 4 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
608 544 adantl ⊢ b = 2 ∧ c = 4 → c ≠ 3
609 608 neneqd ⊢ b = 2 ∧ c = 4 → ¬ c = 3
610 609 olcd ⊢ b = 2 ∧ c = 4 → ¬ b = 2 ∨ ¬ c = 3
611 363 adantr ⊢ b = 2 ∧ c = 4 → b ≠ 3
612 611 neneqd ⊢ b = 2 ∧ c = 4 → ¬ b = 3
613 612 orcd ⊢ b = 2 ∧ c = 4 → ¬ b = 3 ∨ ¬ c = 2
614 610 613 jca ⊢ b = 2 ∧ c = 4 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
615 600 607 614 3jca ⊢ b = 2 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
616 612 orcd ⊢ b = 2 ∧ c = 4 → ¬ b = 3 ∨ ¬ c = 4
617 609 olcd ⊢ b = 2 ∧ c = 4 → ¬ b = 4 ∨ ¬ c = 3
618 616 617 jca ⊢ b = 2 ∧ c = 4 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
619 493 adantr ⊢ b = 2 ∧ c = 4 → b ≠ 4
620 619 neneqd ⊢ b = 2 ∧ c = 4 → ¬ b = 4
621 620 orcd ⊢ b = 2 ∧ c = 4 → ¬ b = 4 ∨ ¬ c = 5
622 402 adantr ⊢ b = 2 ∧ c = 4 → b ≠ 5
623 622 neneqd ⊢ b = 2 ∧ c = 4 → ¬ b = 5
624 623 orcd ⊢ b = 2 ∧ c = 4 → ¬ b = 5 ∨ ¬ c = 4
625 621 624 jca ⊢ b = 2 ∧ c = 4 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
626 593 orcd ⊢ b = 2 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 5
627 596 olcd ⊢ b = 2 ∧ c = 4 → ¬ b = 5 ∨ ¬ c = 0
628 626 627 jca ⊢ b = 2 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
629 618 625 628 3jca ⊢ b = 2 ∧ c = 4 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
630 615 629 jca ⊢ b = 2 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
631 594 597 630 jca31 ⊢ b = 2 ∧ c = 4 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
632 631 olcd ⊢ b = 2 ∧ c = 4 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
633 410 509 632 3jaodan ⊢ b = 2 ∧ c = 0 ∨ c = 2 ∨ c = 4 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
634 446 necon2i ⊢ b = 4 → b ≠ 0
635 634 adantr ⊢ b = 4 ∧ c = 0 → b ≠ 0
636 635 neneqd ⊢ b = 4 ∧ c = 0 → ¬ b = 0
637 636 orcd ⊢ b = 4 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 3
638 229 necon2i ⊢ b = 4 → b ≠ 3
639 638 adantr ⊢ b = 4 ∧ c = 0 → b ≠ 3
640 639 neneqd ⊢ b = 4 ∧ c = 0 → ¬ b = 3
641 640 orcd ⊢ b = 4 ∧ c = 0 → ¬ b = 3 ∨ ¬ c = 0
642 636 orcd ⊢ b = 4 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 1
643 65 necon2i ⊢ b = 4 → b ≠ 1
644 643 adantr ⊢ b = 4 ∧ c = 0 → b ≠ 1
645 644 neneqd ⊢ b = 4 ∧ c = 0 → ¬ b = 1
646 645 orcd ⊢ b = 4 ∧ c = 0 → ¬ b = 1 ∨ ¬ c = 0
647 642 646 jca ⊢ b = 4 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
648 416 necon2i ⊢ c = 0 → c ≠ 2
649 648 adantl ⊢ b = 4 ∧ c = 0 → c ≠ 2
650 649 neneqd ⊢ b = 4 ∧ c = 0 → ¬ c = 2
651 650 olcd ⊢ b = 4 ∧ c = 0 → ¬ b = 1 ∨ ¬ c = 2
652 374 adantl ⊢ b = 4 ∧ c = 0 → c ≠ 1
653 652 neneqd ⊢ b = 4 ∧ c = 0 → ¬ c = 1
654 653 olcd ⊢ b = 4 ∧ c = 0 → ¬ b = 2 ∨ ¬ c = 1
655 651 654 jca ⊢ b = 4 ∧ c = 0 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
656 379 adantl ⊢ b = 4 ∧ c = 0 → c ≠ 3
657 656 neneqd ⊢ b = 4 ∧ c = 0 → ¬ c = 3
658 657 olcd ⊢ b = 4 ∧ c = 0 → ¬ b = 2 ∨ ¬ c = 3
659 640 orcd ⊢ b = 4 ∧ c = 0 → ¬ b = 3 ∨ ¬ c = 2
660 658 659 jca ⊢ b = 4 ∧ c = 0 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
661 647 655 660 3jca ⊢ b = 4 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
662 640 orcd ⊢ b = 4 ∧ c = 0 → ¬ b = 3 ∨ ¬ c = 4
663 657 olcd ⊢ b = 4 ∧ c = 0 → ¬ b = 4 ∨ ¬ c = 3
664 662 663 jca ⊢ b = 4 ∧ c = 0 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
665 389 adantl ⊢ b = 4 ∧ c = 0 → c ≠ 5
666 665 neneqd ⊢ b = 4 ∧ c = 0 → ¬ c = 5
667 666 olcd ⊢ b = 4 ∧ c = 0 → ¬ b = 4 ∨ ¬ c = 5
668 396 adantl ⊢ b = 4 ∧ c = 0 → c ≠ 4
669 668 neneqd ⊢ b = 4 ∧ c = 0 → ¬ c = 4
670 669 olcd ⊢ b = 4 ∧ c = 0 → ¬ b = 5 ∨ ¬ c = 4
671 667 670 jca ⊢ b = 4 ∧ c = 0 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
672 636 orcd ⊢ b = 4 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 5
673 323 necon2i ⊢ b = 4 → b ≠ 5
674 673 adantr ⊢ b = 4 ∧ c = 0 → b ≠ 5
675 674 neneqd ⊢ b = 4 ∧ c = 0 → ¬ b = 5
676 675 orcd ⊢ b = 4 ∧ c = 0 → ¬ b = 5 ∨ ¬ c = 0
677 672 676 jca ⊢ b = 4 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
678 664 671 677 3jca ⊢ b = 4 ∧ c = 0 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
679 661 678 jca ⊢ b = 4 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
680 637 641 679 jca31 ⊢ b = 4 ∧ c = 0 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
681 680 olcd ⊢ b = 4 ∧ c = 0 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
682 634 adantr ⊢ b = 4 ∧ c = 2 → b ≠ 0
683 682 neneqd ⊢ b = 4 ∧ c = 2 → ¬ b = 0
684 683 orcd ⊢ b = 4 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 3
685 416 adantl ⊢ b = 4 ∧ c = 2 → c ≠ 0
686 685 neneqd ⊢ b = 4 ∧ c = 2 → ¬ c = 0
687 686 olcd ⊢ b = 4 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 0
688 683 orcd ⊢ b = 4 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1
689 686 olcd ⊢ b = 4 ∧ c = 2 → ¬ b = 1 ∨ ¬ c = 0
690 688 689 jca ⊢ b = 4 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
691 643 adantr ⊢ b = 4 ∧ c = 2 → b ≠ 1
692 691 neneqd ⊢ b = 4 ∧ c = 2 → ¬ b = 1
693 692 orcd ⊢ b = 4 ∧ c = 2 → ¬ b = 1 ∨ ¬ c = 2
694 420 adantl ⊢ b = 4 ∧ c = 2 → c ≠ 1
695 694 neneqd ⊢ b = 4 ∧ c = 2 → ¬ c = 1
696 695 olcd ⊢ b = 4 ∧ c = 2 → ¬ b = 2 ∨ ¬ c = 1
697 693 696 jca ⊢ b = 4 ∧ c = 2 → ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
698 493 necon2i ⊢ b = 4 → b ≠ 2
699 698 adantr ⊢ b = 4 ∧ c = 2 → b ≠ 2
700 699 neneqd ⊢ b = 4 ∧ c = 2 → ¬ b = 2
701 700 orcd ⊢ b = 4 ∧ c = 2 → ¬ b = 2 ∨ ¬ c = 3
702 638 adantr ⊢ b = 4 ∧ c = 2 → b ≠ 3
703 702 neneqd ⊢ b = 4 ∧ c = 2 → ¬ b = 3
704 703 orcd ⊢ b = 4 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 2
705 701 704 jca ⊢ b = 4 ∧ c = 2 → ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
706 690 697 705 3jca ⊢ b = 4 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
707 703 orcd ⊢ b = 4 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 4
708 411 adantl ⊢ b = 4 ∧ c = 2 → c ≠ 3
709 708 neneqd ⊢ b = 4 ∧ c = 2 → ¬ c = 3
710 709 olcd ⊢ b = 4 ∧ c = 2 → ¬ b = 4 ∨ ¬ c = 3
711 707 710 jca ⊢ b = 4 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
712 455 adantl ⊢ b = 4 ∧ c = 2 → c ≠ 5
713 712 neneqd ⊢ b = 4 ∧ c = 2 → ¬ c = 5
714 713 olcd ⊢ b = 4 ∧ c = 2 → ¬ b = 4 ∨ ¬ c = 5
715 neeq1 ⊢ c = 2 → c ≠ 4 ↔ 2 ≠ 4
716 491 715 mpbiri ⊢ c = 2 → c ≠ 4
717 716 adantl ⊢ b = 4 ∧ c = 2 → c ≠ 4
718 717 neneqd ⊢ b = 4 ∧ c = 2 → ¬ c = 4
719 718 olcd ⊢ b = 4 ∧ c = 2 → ¬ b = 5 ∨ ¬ c = 4
720 714 719 jca ⊢ b = 4 ∧ c = 2 → ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
721 683 orcd ⊢ b = 4 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 5
722 686 olcd ⊢ b = 4 ∧ c = 2 → ¬ b = 5 ∨ ¬ c = 0
723 721 722 jca ⊢ b = 4 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
724 711 720 723 3jca ⊢ b = 4 ∧ c = 2 → ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
725 706 724 jca ⊢ b = 4 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
726 684 687 725 jca31 ⊢ b = 4 ∧ c = 2 → ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
727 726 olcd ⊢ b = 4 ∧ c = 2 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
728 eqtr3 ⊢ b = 4 ∧ c = 4 → b = c
729 728 orcd ⊢ b = 4 ∧ c = 4 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
730 681 727 729 3jaodan ⊢ b = 4 ∧ c = 0 ∨ c = 2 ∨ c = 4 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
731 591 633 730 3jaoian ⊢ b = 0 ∨ b = 2 ∨ b = 4 ∧ c = 0 ∨ c = 2 ∨ c = 4 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
732 540 543 731 syl2anb ⊢ b ∈ G NeighbVtx 3 ∧ c ∈ G NeighbVtx 3 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
733 732 rgen2 ⊢ ∀ b ∈ G NeighbVtx 3 ∀ c ∈ G NeighbVtx 3 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
734 1 2 3 usgrexmpl2nb4 ⊢ G NeighbVtx 4 = 3 5
735 734 eleq2i ⊢ b ∈ G NeighbVtx 4 ↔ b ∈ 3 5
736 6 elpr ⊢ b ∈ 3 5 ↔ b = 3 ∨ b = 5
737 735 736 bitri ⊢ b ∈ G NeighbVtx 4 ↔ b = 3 ∨ b = 5
738 734 eleq2i ⊢ c ∈ G NeighbVtx 4 ↔ c ∈ 3 5
739 10 elpr ⊢ c ∈ 3 5 ↔ c = 3 ∨ c = 5
740 738 739 bitri ⊢ c ∈ G NeighbVtx 4 ↔ c = 3 ∨ c = 5
741 191 341 243 343 ccase ⊢ b = 3 ∨ b = 5 ∧ c = 3 ∨ c = 5 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
742 737 740 741 syl2anb ⊢ b ∈ G NeighbVtx 4 ∧ c ∈ G NeighbVtx 4 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
743 742 rgen2 ⊢ ∀ b ∈ G NeighbVtx 4 ∀ c ∈ G NeighbVtx 4 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
744 1 2 3 usgrexmpl2nb5 ⊢ G NeighbVtx 5 = 0 4
745 744 eleq2i ⊢ b ∈ G NeighbVtx 5 ↔ b ∈ 0 4
746 6 elpr ⊢ b ∈ 0 4 ↔ b = 0 ∨ b = 4
747 745 746 bitri ⊢ b ∈ G NeighbVtx 5 ↔ b = 0 ∨ b = 4
748 744 eleq2i ⊢ c ∈ G NeighbVtx 5 ↔ c ∈ 0 4
749 10 elpr ⊢ c ∈ 0 4 ↔ c = 0 ∨ c = 4
750 748 749 bitri ⊢ c ∈ G NeighbVtx 5 ↔ c = 0 ∨ c = 4
751 356 681 590 729 ccase ⊢ b = 0 ∨ b = 4 ∧ c = 0 ∨ c = 4 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
752 747 750 751 syl2anb ⊢ b ∈ G NeighbVtx 5 ∧ c ∈ G NeighbVtx 5 → b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
753 752 rgen2 ⊢ ∀ b ∈ G NeighbVtx 5 ∀ c ∈ G NeighbVtx 5 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
754 3ex ⊢ 3 ∈ V
755 4nn0 ⊢ 4 ∈ ℕ 0
756 755 elexi ⊢ 4 ∈ V
757 5nn0 ⊢ 5 ∈ ℕ 0
758 757 elexi ⊢ 5 ∈ V
759 oveq2 ⊢ a = 3 → G NeighbVtx a = G NeighbVtx 3
760 759 raleqdv ⊢ a = 3 → ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ c ∈ G NeighbVtx 3 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
761 759 760 raleqbidv ⊢ a = 3 → ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ b ∈ G NeighbVtx 3 ∀ c ∈ G NeighbVtx 3 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
762 oveq2 ⊢ a = 4 → G NeighbVtx a = G NeighbVtx 4
763 762 raleqdv ⊢ a = 4 → ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ c ∈ G NeighbVtx 4 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
764 762 763 raleqbidv ⊢ a = 4 → ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ b ∈ G NeighbVtx 4 ∀ c ∈ G NeighbVtx 4 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
765 oveq2 ⊢ a = 5 → G NeighbVtx a = G NeighbVtx 5
766 765 raleqdv ⊢ a = 5 → ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ c ∈ G NeighbVtx 5 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
767 765 766 raleqbidv ⊢ a = 5 → ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ b ∈ G NeighbVtx 5 ∀ c ∈ G NeighbVtx 5 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
768 754 756 758 761 764 767 raltp ⊢ ∀ a ∈ 3 4 5 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ b ∈ G NeighbVtx 3 ∀ c ∈ G NeighbVtx 3 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ∧ ∀ b ∈ G NeighbVtx 4 ∀ c ∈ G NeighbVtx 4 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ∧ ∀ b ∈ G NeighbVtx 5 ∀ c ∈ G NeighbVtx 5 b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
769 733 743 753 768 mpbir3an ⊢ ∀ a ∈ 3 4 5 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
770 ralunb ⊢ ∀ a ∈ 0 1 2 ∪ 3 4 5 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ a ∈ 0 1 2 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ∧ ∀ a ∈ 3 4 5 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
771 536 769 770 mpbir2an ⊢ ∀ a ∈ 0 1 2 ∪ 3 4 5 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
772 ianor ⊢ ¬ b ≠ c ∧ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ ¬ b ≠ c ∨ ¬ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
773 nne ⊢ ¬ b ≠ c ↔ b = c
774 ioran ⊢ ¬ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ∨ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ∨ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ∧ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ∨ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0
775 ioran ⊢ ¬ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ↔ ¬ b = 0 ∧ c = 3 ∧ ¬ b = 3 ∧ c = 0
776 ianor ⊢ ¬ b = 0 ∧ c = 3 ↔ ¬ b = 0 ∨ ¬ c = 3
777 ianor ⊢ ¬ b = 3 ∧ c = 0 ↔ ¬ b = 3 ∨ ¬ c = 0
778 776 777 anbi12i ⊢ ¬ b = 0 ∧ c = 3 ∧ ¬ b = 3 ∧ c = 0 ↔ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0
779 775 778 bitri ⊢ ¬ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ↔ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0
780 ioran ⊢ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ∨ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ∧ ¬ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0
781 3ioran ⊢ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ↔ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∧ ¬ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∧ ¬ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2
782 ioran ⊢ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ↔ ¬ b = 0 ∧ c = 1 ∧ ¬ b = 1 ∧ c = 0
783 ianor ⊢ ¬ b = 0 ∧ c = 1 ↔ ¬ b = 0 ∨ ¬ c = 1
784 ianor ⊢ ¬ b = 1 ∧ c = 0 ↔ ¬ b = 1 ∨ ¬ c = 0
785 783 784 anbi12i ⊢ ¬ b = 0 ∧ c = 1 ∧ ¬ b = 1 ∧ c = 0 ↔ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
786 782 785 bitri ⊢ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ↔ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0
787 ioran ⊢ ¬ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ↔ ¬ b = 1 ∧ c = 2 ∧ ¬ b = 2 ∧ c = 1
788 ianor ⊢ ¬ b = 1 ∧ c = 2 ↔ ¬ b = 1 ∨ ¬ c = 2
789 ianor ⊢ ¬ b = 2 ∧ c = 1 ↔ ¬ b = 2 ∨ ¬ c = 1
790 788 789 anbi12i ⊢ ¬ b = 1 ∧ c = 2 ∧ ¬ b = 2 ∧ c = 1 ↔ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
791 787 790 bitri ⊢ ¬ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ↔ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1
792 ioran ⊢ ¬ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ↔ ¬ b = 2 ∧ c = 3 ∧ ¬ b = 3 ∧ c = 2
793 ianor ⊢ ¬ b = 2 ∧ c = 3 ↔ ¬ b = 2 ∨ ¬ c = 3
794 ianor ⊢ ¬ b = 3 ∧ c = 2 ↔ ¬ b = 3 ∨ ¬ c = 2
795 793 794 anbi12i ⊢ ¬ b = 2 ∧ c = 3 ∧ ¬ b = 3 ∧ c = 2 ↔ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
796 792 795 bitri ⊢ ¬ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ↔ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
797 786 791 796 3anbi123i ⊢ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∧ ¬ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∧ ¬ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ↔ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
798 781 797 bitri ⊢ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ↔ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2
799 3ioran ⊢ ¬ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∧ ¬ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∧ ¬ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0
800 ioran ⊢ ¬ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ↔ ¬ b = 3 ∧ c = 4 ∧ ¬ b = 4 ∧ c = 3
801 ianor ⊢ ¬ b = 3 ∧ c = 4 ↔ ¬ b = 3 ∨ ¬ c = 4
802 ianor ⊢ ¬ b = 4 ∧ c = 3 ↔ ¬ b = 4 ∨ ¬ c = 3
803 801 802 anbi12i ⊢ ¬ b = 3 ∧ c = 4 ∧ ¬ b = 4 ∧ c = 3 ↔ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
804 800 803 bitri ⊢ ¬ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ↔ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3
805 ioran ⊢ ¬ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ↔ ¬ b = 4 ∧ c = 5 ∧ ¬ b = 5 ∧ c = 4
806 ianor ⊢ ¬ b = 4 ∧ c = 5 ↔ ¬ b = 4 ∨ ¬ c = 5
807 ianor ⊢ ¬ b = 5 ∧ c = 4 ↔ ¬ b = 5 ∨ ¬ c = 4
808 806 807 anbi12i ⊢ ¬ b = 4 ∧ c = 5 ∧ ¬ b = 5 ∧ c = 4 ↔ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
809 805 808 bitri ⊢ ¬ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ↔ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4
810 ioran ⊢ ¬ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 0 ∧ c = 5 ∧ ¬ b = 5 ∧ c = 0
811 ianor ⊢ ¬ b = 0 ∧ c = 5 ↔ ¬ b = 0 ∨ ¬ c = 5
812 ianor ⊢ ¬ b = 5 ∧ c = 0 ↔ ¬ b = 5 ∨ ¬ c = 0
813 811 812 anbi12i ⊢ ¬ b = 0 ∧ c = 5 ∧ ¬ b = 5 ∧ c = 0 ↔ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
814 810 813 bitri ⊢ ¬ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
815 804 809 814 3anbi123i ⊢ ¬ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∧ ¬ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∧ ¬ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
816 799 815 bitri ⊢ ¬ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
817 798 816 anbi12i ⊢ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ∧ ¬ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
818 780 817 bitri ⊢ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ∨ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
819 779 818 anbi12i ⊢ ¬ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ∧ ¬ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ∨ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
820 774 819 bitri ⊢ ¬ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ∨ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ∨ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0 ↔ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
821 6 10 523 524 preq12b ⊢ b c = 0 1 ↔ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0
822 6 10 524 525 preq12b ⊢ b c = 1 2 ↔ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1
823 6 10 525 754 preq12b ⊢ b c = 2 3 ↔ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2
824 821 822 823 3orbi123i ⊢ b c = 0 1 ∨ b c = 1 2 ∨ b c = 2 3 ↔ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2
825 6 10 754 756 preq12b ⊢ b c = 3 4 ↔ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3
826 6 10 756 758 preq12b ⊢ b c = 4 5 ↔ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4
827 6 10 523 758 preq12b ⊢ b c = 0 5 ↔ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0
828 825 826 827 3orbi123i ⊢ b c = 3 4 ∨ b c = 4 5 ∨ b c = 0 5 ↔ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0
829 824 828 orbi12i ⊢ b c = 0 1 ∨ b c = 1 2 ∨ b c = 2 3 ∨ b c = 3 4 ∨ b c = 4 5 ∨ b c = 0 5 ↔ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ∨ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0
830 829 orbi2i ⊢ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ∨ b c = 0 1 ∨ b c = 1 2 ∨ b c = 2 3 ∨ b c = 3 4 ∨ b c = 4 5 ∨ b c = 0 5 ↔ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ∨ b = 0 ∧ c = 1 ∨ b = 1 ∧ c = 0 ∨ b = 1 ∧ c = 2 ∨ b = 2 ∧ c = 1 ∨ b = 2 ∧ c = 3 ∨ b = 3 ∧ c = 2 ∨ b = 3 ∧ c = 4 ∨ b = 4 ∧ c = 3 ∨ b = 4 ∧ c = 5 ∨ b = 5 ∧ c = 4 ∨ b = 0 ∧ c = 5 ∨ b = 5 ∧ c = 0
831 820 830 xchnxbir ⊢ ¬ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ∨ b c = 0 1 ∨ b c = 1 2 ∨ b c = 2 3 ∨ b c = 3 4 ∨ b c = 4 5 ∨ b c = 0 5 ↔ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
832 elun ⊢ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ b c ∈ 0 3 ∨ b c ∈ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
833 prex ⊢ b c ∈ V
834 833 elsn ⊢ b c ∈ 0 3 ↔ b c = 0 3
835 6 10 523 754 preq12b ⊢ b c = 0 3 ↔ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0
836 834 835 bitri ⊢ b c ∈ 0 3 ↔ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0
837 elun ⊢ b c ∈ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ b c ∈ 0 1 1 2 2 3 ∨ b c ∈ 3 4 4 5 0 5
838 833 eltp ⊢ b c ∈ 0 1 1 2 2 3 ↔ b c = 0 1 ∨ b c = 1 2 ∨ b c = 2 3
839 833 eltp ⊢ b c ∈ 3 4 4 5 0 5 ↔ b c = 3 4 ∨ b c = 4 5 ∨ b c = 0 5
840 838 839 orbi12i ⊢ b c ∈ 0 1 1 2 2 3 ∨ b c ∈ 3 4 4 5 0 5 ↔ b c = 0 1 ∨ b c = 1 2 ∨ b c = 2 3 ∨ b c = 3 4 ∨ b c = 4 5 ∨ b c = 0 5
841 837 840 bitri ⊢ b c ∈ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ b c = 0 1 ∨ b c = 1 2 ∨ b c = 2 3 ∨ b c = 3 4 ∨ b c = 4 5 ∨ b c = 0 5
842 836 841 orbi12i ⊢ b c ∈ 0 3 ∨ b c ∈ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ∨ b c = 0 1 ∨ b c = 1 2 ∨ b c = 2 3 ∨ b c = 3 4 ∨ b c = 4 5 ∨ b c = 0 5
843 832 842 bitri ⊢ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ b = 0 ∧ c = 3 ∨ b = 3 ∧ c = 0 ∨ b c = 0 1 ∨ b c = 1 2 ∨ b c = 2 3 ∨ b c = 3 4 ∨ b c = 4 5 ∨ b c = 0 5
844 831 843 xchnxbir ⊢ ¬ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
845 773 844 orbi12i ⊢ ¬ b ≠ c ∨ ¬ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0
846 772 845 bitr2i ⊢ b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ¬ b ≠ c ∧ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
847 846 3ralbii ⊢ ∀ a ∈ 0 1 2 ∪ 3 4 5 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ∀ a ∈ 0 1 2 ∪ 3 4 5 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a ¬ b ≠ c ∧ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
848 ralnex3 ⊢ ∀ a ∈ 0 1 2 ∪ 3 4 5 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a ¬ b ≠ c ∧ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 ↔ ¬ ∃ a ∈ 0 1 2 ∪ 3 4 5 ∃ b ∈ G NeighbVtx a ∃ c ∈ G NeighbVtx a b ≠ c ∧ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
849 847 848 bitri ⊢ ∀ a ∈ 0 1 2 ∪ 3 4 5 ∀ b ∈ G NeighbVtx a ∀ c ∈ G NeighbVtx a b = c ∨ ¬ b = 0 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 0 ∧ ¬ b = 0 ∨ ¬ c = 1 ∧ ¬ b = 1 ∨ ¬ c = 0 ∧ ¬ b = 1 ∨ ¬ c = 2 ∧ ¬ b = 2 ∨ ¬ c = 1 ∧ ¬ b = 2 ∨ ¬ c = 3 ∧ ¬ b = 3 ∨ ¬ c = 2 ∧ ¬ b = 3 ∨ ¬ c = 4 ∧ ¬ b = 4 ∨ ¬ c = 3 ∧ ¬ b = 4 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 4 ∧ ¬ b = 0 ∨ ¬ c = 5 ∧ ¬ b = 5 ∨ ¬ c = 0 ↔ ¬ ∃ a ∈ 0 1 2 ∪ 3 4 5 ∃ b ∈ G NeighbVtx a ∃ c ∈ G NeighbVtx a b ≠ c ∧ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
850 771 849 mpbi ⊢ ¬ ∃ a ∈ 0 1 2 ∪ 3 4 5 ∃ b ∈ G NeighbVtx a ∃ c ∈ G NeighbVtx a b ≠ c ∧ b c ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
851 1 2 3 usgrexmpl2 ⊢ G ∈ USGraph
852 1 2 3 usgrexmpl2vtx ⊢ Vtx ⁡ G = 0 1 2 ∪ 3 4 5
853 852 eqcomi ⊢ 0 1 2 ∪ 3 4 5 = Vtx ⁡ G
854 1 2 3 usgrexmpl2edg ⊢ Edg ⁡ G = 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
855 854 eqcomi ⊢ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 = Edg ⁡ G
856 eqid ⊢ G NeighbVtx a = G NeighbVtx a
857 853 855 856 usgrgrtrirex Could not format ( G e. USGraph -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) ) ) : No typesetting found for |- ( G e. USGraph -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) ) ) with typecode |-
858 851 857 ax-mp Could not format ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) ) : No typesetting found for |- ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) ) with typecode |-
859 850 858 mtbir Could not format -. E. t t e. ( GrTriangles ` G ) : No typesetting found for |- -. E. t t e. ( GrTriangles ` G ) with typecode |-