diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean
index 5e412f36..3af92f94 100644
--- a/equational_theories/Subgraph.lean
+++ b/equational_theories/Subgraph.lean
@@ -105,9 +105,15 @@ theorem Equation5_implies_Equation4512 (G: Type*) [Magma G] (h: Equation5 G) : E
 theorem Equation6_implies_Equation2 (G: Type*) [Magma G] (h: Equation6 G) : Equation2 G :=
   fun a _ ↦ by rw [h a a, ← h]
 
+theorem Equation6_implies_Equation3 (G: Type*) [Magma G] (h: Equation6 G) : Equation3 G :=
+  fun _ ↦ h _ _
+
 theorem Equation7_implies_Equation2 (G: Type*) [Magma G] (h: Equation7 G) : Equation2 G :=
   fun a _ ↦ by rw [h a a a, ← h]
 
+theorem Equation7_implies_Equation3 (G: Type*) [Magma G] (h: Equation7 G) : Equation3 G :=
+  fun _ ↦ h _ _ _
+
 theorem Equation7_implies_Equation41 (G: Type*) [Magma G] (h: Equation7 G) : Equation41 G :=
   fun _ _ _ ↦ by rw [← h]