Every graph with no $K_7^{=}$ minor is 6-colorable

The first open case of Hadwiger’s conjecture states that every $K_7$-minor-free graph is 6-colorable. We prove that this is the case for $K_7^{=}$-minor-free graphs, where $K_7^{=}$ denotes the graph obtained from $K_7$ by deleting two independent edges. The proof is based on an independently interesting density result: Every 5-connected $K_7^{=}$-minor-free graph with $n\ge 6$ vertices has at most $4n-8$ edges.