diff --git a/CHANGELOG.md b/CHANGELOG.md
index 76ca38cd42..57c59a10fd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1601,8 +1601,30 @@ Other minor changes
                                      Involutive _≈_ f
   ```
 
+* Added new proofs to `Algebra.Consequences.Propositional`:
+  ```agda
+  comm+assoc⇒middleFour     : Commutative _•_ →
+                              Associative _•_ →
+                              _•_ MiddleFourExchange _•_
+  identity+middleFour⇒assoc : Identity e _•_ →
+                              _•_ MiddleFourExchange _•_ →
+                              Associative _•_
+  identity+middleFour⇒comm  : Identity e _+_ →
+                              _•_ MiddleFourExchange _+_ →
+                              Commutative _•_
+  ```
+
 * Added new proofs to `Algebra.Consequences.Setoid`:
   ```agda
+  comm+assoc⇒middleFour     : Congruent₂ _•_ → Commutative _•_ → Associative _•_ →
+                              _•_ MiddleFourExchange _•_
+  identity+middleFour⇒assoc : Congruent₂ _•_ → Identity e _•_ →
+                              _•_ MiddleFourExchange _•_ →
+                              Associative _•_
+  identity+middleFour⇒comm  : Congruent₂ _•_ → Identity e _+_ →
+                              _•_ MiddleFourExchange _+_ →
+                              Commutative _•_
+
   involutive⇒surjective  : Involutive f  → Surjective f
   selfInverse⇒involutive : SelfInverse f → Involutive f
   selfInverse⇒congruent  : SelfInverse f → Congruent f
@@ -1666,6 +1688,8 @@ Other minor changes
 
 * Added new definition to `Algebra.Definitions`:
   ```agda
+  _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
+
   SelfInverse : Op₁ A → Set _
   
   LeftDividesˡ  : Op₂ A → Op₂ A → Set _
diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda
index 05278fea34..7c3030f4a6 100644
--- a/src/Algebra/Consequences/Propositional.agda
+++ b/src/Algebra/Consequences/Propositional.agda
@@ -24,7 +24,10 @@ import Algebra.Consequences.Setoid (setoid A) as Base
 
 open Base public
   hiding
-  ( assoc+distribʳ+idʳ+invʳ⇒zeˡ
+  ( comm+assoc⇒middleFour
+  ; identity+middleFour⇒assoc
+  ; identity+middleFour⇒comm
+  ; assoc+distribʳ+idʳ+invʳ⇒zeˡ
   ; assoc+distribˡ+idʳ+invʳ⇒zeʳ
   ; assoc+id+invʳ⇒invˡ-unique
   ; assoc+id+invˡ⇒invʳ-unique
@@ -90,6 +93,25 @@ module _ {_•_ : Op₂ A} where
   sel⇒idem : Selective _•_ → Idempotent _•_
   sel⇒idem = Base.sel⇒idem _≡_
 
+------------------------------------------------------------------------
+-- Middle-Four Exchange
+
+module _ {_•_ : Op₂ A} where
+
+  comm+assoc⇒middleFour : Commutative _•_ → Associative _•_ →
+                          _•_ MiddleFourExchange _•_
+  comm+assoc⇒middleFour = Base.comm+assoc⇒middleFour (cong₂ _•_)
+
+  identity+middleFour⇒assoc : {e : A} → Identity e _•_ →
+                              _•_ MiddleFourExchange _•_ →
+                              Associative _•_
+  identity+middleFour⇒assoc = Base.identity+middleFour⇒assoc (cong₂ _•_)
+
+  identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
+                             _•_ MiddleFourExchange _+_ →
+                             Commutative _•_
+  identity+middleFour⇒comm = Base.identity+middleFour⇒comm (cong₂ _•_)
+
 ------------------------------------------------------------------------
 -- Without Loss of Generality
 
diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index c51a6ee8b1..77badd1b90 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -29,6 +29,40 @@ open import Relation.Unary using (Pred)
 
 open import Algebra.Consequences.Base public
 
+------------------------------------------------------------------------
+-- MiddleFourExchange
+
+module _ {_•_ : Op₂ A} (cong : Congruent₂ _•_) where
+
+  comm+assoc⇒middleFour : Commutative _•_ → Associative _•_ →
+                          _•_ MiddleFourExchange _•_
+  comm+assoc⇒middleFour comm assoc w x y z = begin
+    (w • x) • (y • z) ≈⟨ assoc w x (y • z) ⟩
+    w • (x • (y • z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩
+    w • ((x • y) • z) ≈⟨ cong refl (cong (comm x y) refl) ⟩
+    w • ((y • x) • z) ≈⟨ cong refl (assoc y x z) ⟩
+    w • (y • (x • z)) ≈⟨ sym (assoc w y (x • z)) ⟩
+    (w • y) • (x • z) ∎
+
+  identity+middleFour⇒assoc : {e : A} → Identity e _•_ →
+                              _•_ MiddleFourExchange _•_ →
+                              Associative _•_
+  identity+middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
+    (x • y) • z       ≈⟨ cong refl (sym (identityˡ z)) ⟩
+    (x • y) • (e • z) ≈⟨ middleFour x y e z ⟩
+    (x • e) • (y • z) ≈⟨ cong (identityʳ x) refl ⟩
+    x • (y • z)       ∎
+
+  identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
+                             _•_ MiddleFourExchange _+_ →
+                             Commutative _•_
+  identity+middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
+    = begin
+    x • y             ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩
+    (e + x) • (y + e) ≈⟨ middleFour e x y e ⟩
+    (e + y) • (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
+    y • x             ∎
+
 ------------------------------------------------------------------------
 -- Involutive/SelfInverse functions
 
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index e9e082e7e1..c0820fafb7 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -108,6 +108,10 @@ _*_ DistributesOverʳ _+_ =
 _DistributesOver_ : Op₂ A → Op₂ A → Set _
 * DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
 
+_MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
+_*_ MiddleFourExchange _+_ = 
+  ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z))
+
 _IdempotentOn_ : Op₂ A → A → Set _
 _∙_ IdempotentOn x = (x ∙ x) ≈ x