Proving $\vdash_{HPI}A\vee(B\vee C) \rightarrow (A\vee B)\vee C $ Prove $\vdash_{HPI}A\vee(B\vee C) \rightarrow (A\vee B)\vee C $
From the axioms :
A1) A→(B→A)
A2) (A→(B→C))→((A→B)→(A→C))
A3) $(A\rightarrow B)\rightarrow((A\rightarrow\neg B)\rightarrow \neg A)$
A4) $\neg A\rightarrow A\rightarrow B$
A5) (A∧B)→A
A6) (A∧B)→B
A7) A→(B→(A∧B))
A8) A→(A∨B)
A9) B→(A∨B)
A10) (A→B)→((C→B)→((A∨C)→B))
and MP
I know by the deduction theorem it is enough to show $A\vee(B\vee C) \vdash_{HPI} (A\vee B)\vee C $.
It's clearly true because of associativity. However, I'm not sure how to prove it formally using only the axioms above.
Thanks
 A: In the Hilbert-style proof system for propositional calculus above, we can use the "derived rule" of Hypothetical Syllogism :

$A \to B, B \to C \vdash A \to C$.

With it, we have:
1) $B \to (A \lor B)$
2) $(A \lor B) \to (A \lor B) \lor C$
3) $B \to (A \lor B) \lor C$ --- from 1) and 2) by HS
4) $C \to (A \lor B) \lor C$

5) $B \lor C \to (A \lor B) \lor C$ --- from 3) and 4) by A10) and Modus Ponens twice

6) $A \to (A \lor B)$
7) $(A \lor B) \to (A \lor B) \lor C$

8) $A \to (A \lor B) \lor C$ --- from 6) and 7) by HS

9) $A \lor (B \lor C) \to (A \lor B) \lor C$ --- from 5) and 8) by A10) and Modus Ponens twice.



In order to prove Hypothetical Syllogism, we have :


*

*$A \rightarrow B$ --- premise

*$B \rightarrow C$ --- premise

*$(B \rightarrow C) \rightarrow  (A \rightarrow (B \rightarrow C))$ --- A1)

*$A \rightarrow (B \rightarrow C)$ --- from 2) and 3) by MP

*$(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$ --- A2)

*$(A \rightarrow B) \rightarrow (A \rightarrow C)$ --- from 4) and 5) by MP


  
*$A \rightarrow C$ --- from 1) and 6) by MP.
  

