diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean
index 15d24bcaac..3d1cecdf32 100644
--- a/src/Init/SimpLemmas.lean
+++ b/src/Init/SimpLemmas.lean
@@ -156,6 +156,9 @@ theorem dite_congr {s : Decidable b} [Decidable c]
 @[simp] theorem beq_self_eq_true [BEq α] [LawfulBEq α] (a : α) : (a == a) = true := LawfulBEq.rfl
 @[simp] theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true := by simp [BEq.beq]
 
+@[simp] theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false := by simp [bne]
+@[simp] theorem bne_self_eq_false' [DecidableEq α] (a : α) : (a != a) = false := by simp [bne]
+
 @[simp] theorem Nat.le_zero_eq (a : Nat) : (a ≤ 0) = (a = 0) :=
   propext <| Iff.intro (fun h => Nat.le_antisymm h (Nat.zero_le ..)) (fun h => by simp [h])