diff --git a/Mathlib.lean b/Mathlib.lean
index 92e3cf81853411..49a4130a24ce7c 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5979,6 +5979,7 @@ public import Mathlib.Order.CountableSupClosed
 public import Mathlib.Order.Cover
 public import Mathlib.Order.Defs.LinearOrder
 public import Mathlib.Order.Defs.PartialOrder
+public import Mathlib.Order.Defs.Prop
 public import Mathlib.Order.Defs.Unbundled
 public import Mathlib.Order.DirSupClosed
 public import Mathlib.Order.Directed
diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
index d03d6ac2f44b9d..24ba1c2d27cb80 100644
--- a/Mathlib/Order/Basic.lean
+++ b/Mathlib/Order/Basic.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Data.Subtype
 public import Mathlib.Order.Defs.LinearOrder
+public import Mathlib.Order.Defs.Prop
 public import Mathlib.Order.Notation
 public import Mathlib.Tactic.Spread
 public import Mathlib.Tactic.Convert
@@ -549,15 +550,6 @@ instance Ne.instIsEquiv_compl : IsEquiv α (· ≠ ·)ᶜ := by
 
 /-! ### Order instances on the function space -/
 
-
-instance Pi.hasLe [∀ i, LE (π i)] :
-    LE (∀ i, π i) where le x y := ∀ i, x i ≤ y i
-
-@[to_dual self]
-theorem Pi.le_def [∀ i, LE (π i)] {x y : ∀ i, π i} :
-    x ≤ y ↔ ∀ i, x i ≤ y i :=
-  Iff.rfl
-
 instance Pi.preorder [∀ i, Preorder (π i)] : Preorder (∀ i, π i) where
   __ := (inferInstance : LE (∀ i, π i))
   le_refl := fun a i ↦ le_refl (a i)
@@ -1098,14 +1090,6 @@ end PUnit
 
 section «Prop»
 
-/-- Propositions form a complete Boolean algebra, where the `≤` relation is given by implication. -/
-instance Prop.le : LE Prop :=
-  ⟨(· → ·)⟩
-
-@[simp]
-theorem le_Prop_eq : ((· ≤ ·) : Prop → Prop → Prop) = (· → ·) :=
-  rfl
-
 theorem subrelation_iff_le {r s : α → α → Prop} : Subrelation r s ↔ r ≤ s :=
   Iff.rfl
 
diff --git a/Mathlib/Order/Defs/Prop.lean b/Mathlib/Order/Defs/Prop.lean
new file mode 100644
index 00000000000000..2491ab8634ff70
--- /dev/null
+++ b/Mathlib/Order/Defs/Prop.lean
@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2016 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Yury Kudryashov
+-/
+module
+
+import Mathlib.Tactic.ToDual
+
+/-!
+# Order definitions for propositions
+
+This file defines orders on `Pi` and `Prop`.
+-/
+
+public section
+
+instance Pi.hasLe {ι : Type*} {π : ι → Type*} [∀ i, LE (π i)] : LE (∀ i, π i) where
+  le x y := ∀ i, x i ≤ y i
+
+@[to_dual self]
+theorem Pi.le_def {ι : Type*} {π : ι → Type*} [∀ i, LE (π i)] {x y : ∀ i, π i} :
+    x ≤ y ↔ ∀ i, x i ≤ y i :=
+  .rfl
+
+/-- Propositions form a complete Boolean algebra, where the `≤` relation is given by implication. -/
+instance Prop.le : LE Prop :=
+  ⟨(· → ·)⟩
+
+@[simp]
+theorem le_Prop_eq : ((· ≤ ·) : Prop → Prop → Prop) = (· → ·) :=
+  rfl