private void checkValidMpMt(String[] Lines, String reason, String expr) throws IllegalInferenceException, IllegalLineException {
		Expression validAssumptions; //Form of ((E1=>E2)&E3)=>E4). E's depends on reason used.
		Expression reasonTh;
		if (ProofChecker.iAmDebugging) {
			System.out.println("Reason is "+reason);
		}
		if (reason.equals("mp")) {
			reasonTh = new Expression("((p&(p=>q))=>q)");
			if (ProofChecker.iAmDebugging){
				System.out.println("Theorem is "+reasonTh.toString());
			}
		} else {
			reasonTh = new Expression("((~q&(p=>q))=>~p)");
			if (ProofChecker.iAmDebugging){
				System.out.println("Theorem is "+reasonTh.toString());
			}
		}
		try { //assume that E1 is the first input
			validAssumptions = new Expression("(("+AssumeProven.get(Lines[0]).toString()+"&"
					+AssumeProven.get(Lines[1]).toString()+")=>"+expr.toString()+")");
			if (ProofChecker.iAmDebugging) {
				System.out.println(validAssumptions.toString());
			}
			TheoremChecker testmatch = new TheoremChecker(reasonTh,validAssumptions); 
			//if assumption is false, it will throw an IllegalInferenceException
			if (ProofChecker.iAmDebugging) {
				System.out.println("The theorem matches: "+testmatch.matches());
			}
		} catch (IllegalInferenceException e) { //switch arguments and try again
			validAssumptions = new Expression("(("+AssumeProven.get(Lines[1]).toString()+"&"
					+AssumeProven.get(Lines[0]).toString()+")=>"+expr.toString()+")");
			if (ProofChecker.iAmDebugging) {
				System.out.println(validAssumptions.toString());
			}
			TheoremChecker testMatch = new TheoremChecker(reasonTh,validAssumptions); 
			//if it still does not match, it will throw IllegalInferenceException
			if (ProofChecker.iAmDebugging) {
				System.out.println("The theorem matches: "+testMatch.matches());
			}
		}
	}