diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 165b9e4debac..5a58f0623595 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -243,6 +243,15 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
 
 @[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl
 
+@[simp] theorem ofBool_and_ofBool : ofBool b &&& ofBool b' = ofBool (b && b') := by
+  cases b <;> cases b' <;> rfl
+
+@[simp] theorem ofBool_or_ofBool : ofBool b ||| ofBool b' = ofBool (b || b') := by
+  cases b <;> cases b' <;> rfl
+
+@[simp] theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by
+  cases b <;> cases b' <;> rfl
+
 @[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
 
 @[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out
index 3dff7f4398fa..aaa1f429ac26 100644
--- a/tests/lean/interactive/completionPrv.lean.expected.out
+++ b/tests/lean/interactive/completionPrv.lean.expected.out
@@ -46,6 +46,30 @@
      "position": {"line": 9, "character": 11}},
     "id": {"const": {"declName": "BitVec.getMsbD_ofBoolListBE"}}}},
   {"sortText": "4",
+   "label": "BitVec.ofBool_and_ofBool",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionPrv.lean"},
+     "position": {"line": 9, "character": 11}},
+    "id": {"const": {"declName": "BitVec.ofBool_and_ofBool"}}}},
+  {"sortText": "5",
+   "label": "BitVec.ofBool_or_ofBool",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionPrv.lean"},
+     "position": {"line": 9, "character": 11}},
+    "id": {"const": {"declName": "BitVec.ofBool_or_ofBool"}}}},
+  {"sortText": "6",
+   "label": "BitVec.ofBool_xor_ofBool",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionPrv.lean"},
+     "position": {"line": 9, "character": 11}},
+    "id": {"const": {"declName": "BitVec.ofBool_xor_ofBool"}}}},
+  {"sortText": "7",
    "label": "BitVec.ofBoolListBE",
    "kind": 3,
    "documentation":