diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 22955191a..88879b6a0 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -606,6 +606,11 @@ theorem shiftLeft_add_distrib {x y : BitVec w} {n : Nat} :
     rw [Nat.mod_eq_of_eq]
     omega
 
+@[simp]
+theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} :
+    x <<< n &&& y <<< (m + n) = (x &&& y <<< m) <<< n := by
+  simp [BitVec.shiftLeft_and_distrib, BitVec.shiftLeft_add]
+
 @[simp]
 theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} (n : Nat) :
     BitVec.allOnes w <<< n &&& x <<< n = x <<< n := by