diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 850a760114..b29f991284 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -760,6 +760,7 @@ def Or.symm := @Or.swap
 /- xor -/
 def Xor (a b : Prop) : Prop := (a ∧ ¬ b) ∨ (b ∧ ¬ a)
 
+@[recursor 5]
 theorem Iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c :=
 Iff.rec h₁ h₂
 
diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean
index 19e841103f..d7d7c4e00e 100644
--- a/tests/lean/run/induction1.lean
+++ b/tests/lean/run/induction1.lean
@@ -76,3 +76,9 @@ begin
   | nil       => exact rfl
   | cons z zs => exact absurd rfl (h z zs)
 end
+
+theorem tst10 {p q : Prop } (h₁ : p ↔ q) (h₂ : p) : q :=
+begin
+  induction h₁ using Iff.elim with
+  | _ h _ => exact h h₂
+end