diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 282e31a..24f1615 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -1714,5 +1714,48 @@ mod tests
 			implies_right(if_and_only_if(vec![implies_right(p1(), q1())]),
 				if_and_only_if(vec![implies_right(p2(), q2())]))),
 			"(p1 -> q1) -> p2 -> q2");
+		assert_eq!(format(
+			implies_right(implies_left(p1(), q1()), implies_left(p2(), q2()))),
+			"(q1 <- p1) -> (q2 <- p2)");
+		assert_eq!(format(
+			implies_right(and(vec![implies_left(p1(), q1())]),
+				and(vec![implies_left(p2(), q2())]))),
+			"(q1 <- p1) -> (q2 <- p2)");
+		assert_eq!(format(
+			implies_right(or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]))),
+			"(q1 <- p1) -> (q2 <- p2)");
+		assert_eq!(format(
+			implies_right(if_and_only_if(vec![implies_left(p1(), q1())]),
+				if_and_only_if(vec![implies_left(p2(), q2())]))),
+			"(q1 <- p1) -> (q2 <- p2)");
+		assert_eq!(format(
+			implies_left(implies_right(p1(), q1()), implies_right(p2(), q2()))),
+			"(p2 -> q2) <- (p1 -> q1)");
+		assert_eq!(format(
+			implies_left(and(vec![implies_right(p1(), q1())]),
+				and(vec![implies_right(p2(), q2())]))),
+			"(p2 -> q2) <- (p1 -> q1)");
+		assert_eq!(format(
+			implies_left(or(vec![implies_right(p1(), q1())]), or(vec![implies_right(p2(), q2())]))),
+			"(p2 -> q2) <- (p1 -> q1)");
+		assert_eq!(format(
+			implies_left(if_and_only_if(vec![implies_right(p1(), q1())]),
+				if_and_only_if(vec![implies_right(p2(), q2())]))),
+			"(p2 -> q2) <- (p1 -> q1)");
+		assert_eq!(format(
+			implies_left(implies_left(p1(), q1()), implies_left(p2(), q2()))),
+			"q2 <- p2 <- (q1 <- p1)");
+		assert_eq!(format(
+			implies_left(and(vec![implies_left(p1(), q1())]), and(vec![implies_left(p2(), q2())]))),
+			"q2 <- p2 <- (q1 <- p1)");
+		assert_eq!(format(
+			implies_left(or(vec![implies_left(p1(), q1())]), or(vec![implies_left(p2(), q2())]))),
+			"q2 <- p2 <- (q1 <- p1)");
+		assert_eq!(format(
+			implies_left(if_and_only_if(vec![implies_left(p1(), q1())]),
+				if_and_only_if(vec![implies_left(p2(), q2())]))),
+			"q2 <- p2 <- (q1 <- p1)");
+
+		// TODO: Implies + if and only if
 	}
 }