diff --git a/library/init/logic.lean b/library/init/logic.lean
index f2bb257c8e..26706e3e47 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -817,11 +817,11 @@ lemma if_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] {x y u v :
 @if_ctx_simp_congr α b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e)
 
 @[simp]
-def if_true {α : Type u} (t e : α) : (if true then t else e) = t :=
+def if_true {α : Type u} {h : decidable true} (t e : α) : (@ite true h α t e) = t :=
 if_pos trivial
 
 @[simp]
-def if_false {α : Type u} (t e : α) : (if false then t else e) = e :=
+def if_false {α : Type u} {h : decidable false} (t e : α) : (@ite false h α t e) = e :=
 if_neg not_false
 
 lemma if_ctx_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c]
diff --git a/tests/lean/run/simp_if_true_false.lean b/tests/lean/run/simp_if_true_false.lean
new file mode 100644
index 0000000000..fba9dd22bd
--- /dev/null
+++ b/tests/lean/run/simp_if_true_false.lean
@@ -0,0 +1,2 @@
+example (m n p : ℕ) : ite (m = m) n p = n := by simp
+example (m n p : ℕ) : ite (m ≠ m) n p = p := by simp