private void mt (LineNumber l1, LineNumber l2, Expression prove) throws IllegalLineException, IllegalInferenceException {

		if ((l1.toString().length() > globalLine().toString().length()) ||
				(l2.toString().length() > globalLine().toString().length())) {
			throw new IllegalLineException("Incorrectly referencing line in subproof");
		}
		
		Expression given1 = lookupLine(l1);
		Expression given2 = lookupLine(l2);

		if (given1.getRoot() != '=' && given2.getRoot() != '=') {
			throw new IllegalInferenceException("Not a valid use of modus tollens.");
		}

		if (given2.equals(given1.getRight().negate()) && prove.equals(given1.getLeft().negate()) ||
			given1.equals(given2.getRight().negate()) && prove.equals(given2.getLeft().negate())) {


			if (!check(prove)) {
				addLine(globalLine(), prove);
				increment();
			}
		}

		else {
			throw new IllegalInferenceException("Not a valid use of modus tollens.");
		}
	}