Problem with proving formally tautology using given rules

Question

Using the rules below prove that the following assumeptions leads to the following conclusion by tautology.

$A\vee B \vee C, A\to C, B\to C \Rightarrow C$

What I did:

1. $A\vee B \vee C$ Assumption
2. $A\to C$ Assumption
3. $B\to C$ Assumption
4. $A\vee B\to C$ rule 11 on lines 2,3
5. $\neg\neg(A\lor B \lor C)$ rule 7 on line 1
6. $\neg (\neg A\land \neg B \land \neg C)$ rule 14 on line 5
7. $\neg\neg A$ rule 3 on line 6
8. $A$ rule 7 on line 7
9. $A\vee B$ rule 5 on line 8
10. $C$ rule 1 on line 4, 9 $\square$

But there seems to be a problem since I get that $(A\vee B \vee C)\to A$ which can't be right... So what am I doing wrong here?

Answer 1

I use Polish/Lukasiewicz notation.

Rule 1 says

a, Cab -> b.

Rule 11 (R11) says

Cac, Cbc -> C Aab c

Thus, we'll derive a rule first, which I'll denote R16. The rule is Cac, Cbc, Aab -> c.

assumption 1 Cac
assumption 2 Cbc
assumption 3 Aab
1, 2, R11  4 CAabc
3, 4, R1   5 c

Now we'll solve the problem:

assumption     1 AAabc
assumption     2 Cac
assumption     3 Cbc
2, 3 R11       4 C Aab c
T13, 1, 4, R16 5 c

where T13 is Caa or any substitution instance of it such as Ccc.