diff --git a/__pycache__/logicObjects.cpython-39.pyc b/__pycache__/logicObjects.cpython-39.pyc
index 228e8e8..7285b63 100644
Binary files a/__pycache__/logicObjects.cpython-39.pyc and b/__pycache__/logicObjects.cpython-39.pyc differ
diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc
index 0e857c7..c898826 100644
Binary files a/__pycache__/proof.cpython-39.pyc and b/__pycache__/proof.cpython-39.pyc differ
diff --git a/contradiction_proof.py b/contradiction_proof.py
index a8e489e..dcac2a3 100644
--- a/contradiction_proof.py
+++ b/contradiction_proof.py
@@ -23,4 +23,5 @@
 p.switchSidesOfEqual(8)
 p.notElim(6,9)
 p.concludeSubproof(6)
-#p.impliesIntroduction([4,5],11)
\ No newline at end of file
+p.impliesIntroduction([4,5],11)
+p.qed(12)
diff --git a/logicObjects.py b/logicObjects.py
index 8ec70d7..4075cee 100644
--- a/logicObjects.py
+++ b/logicObjects.py
@@ -70,6 +70,17 @@ def elim(self, arg):
         if arg==self.assum:
             return self.conc
 
+    def __eq__(self, other):
+        return self.assum == other.assum and self.conc == other.conc
+
+    def __repr__(self):
+        assumptionstr = ""
+        for assumption in self.assum:
+            assumptionstr += str(assumption)
+            assumptionstr += ", "
+        assumptionstr = assumptionstr[:-2]
+        return  assumptionstr + " → " +  str(self.conc)
+
 class Not:
     def __init__(self, arg):
         self.arg = arg
diff --git a/proof.py b/proof.py
index 6041010..13e5698 100644
--- a/proof.py
+++ b/proof.py
@@ -615,4 +615,17 @@ def notElim(self, lineNum1, lineNum2):
             self.justifications += [f'Contradiction from lines {lineNum1} and {lineNum2}']
             self.show()
         else:
-            print(f"The statement on line {lineNum1} isn't a Not")
\ No newline at end of file
+            print(f"The statement on line {lineNum1} isn't a Not")
+
+    def impliesIntroduction(self, lineNumsAssums, lineNumConc): # needs work, a lot of it
+        '''
+        Introduce an implication based on assumptions and a conclusion
+        :param lineNumsAssums: the lines containing the assumptions
+        :param lineNumConc: the line to conclude
+        '''
+        assums = []
+        for line in lineNumsAssums:
+            assums.append(self.steps[line])
+        self.steps += [Implies(assums,self.steps[lineNumConc])]
+        self.justifications += [f"Introduced implies based on assumptions on lines {lineNumsAssums} to conclude line {lineNumConc}"]
+        self.show()
\ No newline at end of file