diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean
index c723b9776..ca55b9cdd 100644
--- a/library/logic/quantifiers.lean
+++ b/library/logic/quantifiers.lean
@@ -126,17 +126,14 @@ end
 section
   variables {A : Type} {p₁ p₂ : A → Prop} (H : ∀ x, p₁ x ↔ p₂ x)
 
-  theorem congr_forall [congr] : (∀ x, p₁ x) ↔ (∀ x, p₂ x) :=
+  theorem congr_forall : (∀ x, p₁ x) ↔ (∀ x, p₂ x) :=
   forall_congr H
 
-  theorem congr_exists [congr] : (∃ x, p₁ x) ↔ (∃ x, p₂ x) :=
+  theorem congr_exists : (∃ x, p₁ x) ↔ (∃ x, p₂ x) :=
   exists_congr H
 
   include H
-  theorem congr_exists_unique [congr] : (∃! x, p₁ x) ↔ (∃! x, p₂ x) :=
+  theorem congr_exists_unique : (∃! x, p₁ x) ↔ (∃! x, p₂ x) :=
    congr_exists (λx, congr_and (H x) (congr_forall
      (λy, congr_imp (H y) iff.rfl)))
 end
-
-/- We add this attribute again here so that the simplifier finds it before [congr_forall] -/
-attribute congr_imp [congr]
diff --git a/tests/lean/simplifier6.lean b/tests/lean/simplifier6.lean
index 4a6c11161..963b83bee 100644
--- a/tests/lean/simplifier6.lean
+++ b/tests/lean/simplifier6.lean
@@ -1,6 +1,9 @@
 /- Basic pi congruence -/
 import logic.connectives logic.quantifiers
 
+attribute congr_forall [congr]
+attribute congr_imp [congr]
+
 namespace pi_congr1
 constants (p1 q1 p2 q2 p3 q3 : Prop) (H1 : p1 ↔ q1) (H2 : p2 ↔ q2) (H3 : p3 ↔ q3)
 local attribute H1 [simp]
diff --git a/tests/lean/simplifier9.lean b/tests/lean/simplifier9.lean
index 86e9f2d6b..b3e4a7f75 100644
--- a/tests/lean/simplifier9.lean
+++ b/tests/lean/simplifier9.lean
@@ -1,6 +1,9 @@
 -- Rewriting with (tmp)-local hypotheses
 import logic.quantifiers
 
+attribute congr_forall [congr]
+attribute congr_imp [congr]
+
 universe l
 constants (T : Type.{l}) (P Q : T → Prop)