Does this proof using Novikov axiomatic propositional logic hold? This question seems absolutely elementary but I'm having a hard time completing the proof, in fact I may have taken a bit of a left turn on it or I may be improperly applying axioms all together.  Clearly I'm not asking for a complete solution, but if anyone can offer anything that will increase my insight I would appreciate it..
Prove that $$A \lor A \Rightarrow A$$ using the Novikov axiom system.
The axioms I have are stated as:


*

*$A \Rightarrow (B \Rightarrow A)$

*$(A\Rightarrow(B\Rightarrow C))\Rightarrow((A\Rightarrow B)\Rightarrow(A\Rightarrow C))$

*$A \land B \Rightarrow A$

*$A\land B \Rightarrow B$

*$(A \Rightarrow B)\Rightarrow ((A\Rightarrow C)\Rightarrow (A\Rightarrow B \land C))$

*$A\Rightarrow A\lor B$

*$B\Rightarrow A\lor B$

*$(A\Rightarrow C)\Rightarrow ((B\Rightarrow C)\Rightarrow (A\lor B\Rightarrow C))$

*$(A\Rightarrow B)\Rightarrow(\lnot B \Rightarrow \lnot A)$

*$A \Rightarrow \lnot\lnot A$

*$\lnot\lnot A\Rightarrow A$


We may use a substitution (specialization) and modus ponens.
So based on the idea that I will need to use something more expanded to start with and try to contract it:
Start with 8:
$(A\Rightarrow C)\Rightarrow ((B\Rightarrow C)\Rightarrow (A\lor B\Rightarrow C))$
Apply 6:
$(A\Rightarrow C)\Rightarrow ((B\Rightarrow C)\Rightarrow (A \Rightarrow C))$
Apply 6:
$(A \lor B\Rightarrow C)\Rightarrow ((B\Rightarrow C)\Rightarrow (A \lor B \Rightarrow C))$
Apply 7:
$(A \lor A \lor B\Rightarrow C)\Rightarrow ((A \lor B\Rightarrow C)\Rightarrow (A \lor A \lor B \Rightarrow C))$
Apply 6:
$(A \lor A \Rightarrow C)\Rightarrow ((A \Rightarrow C)\Rightarrow (A \lor A
 \Rightarrow C))$
Apply 3: (rearranging A and C using rename rules)
$(A \lor A \Rightarrow A \land C)\Rightarrow ((A \Rightarrow A \land C)\Rightarrow (A \lor A \Rightarrow A \land C))$
Apply 3:
$(A \lor A \Rightarrow A)\Rightarrow ((A \Rightarrow A)\Rightarrow (A \lor A \Rightarrow A))$
Apply 1:
$(A \lor A)\Rightarrow ((A)\Rightarrow (A \lor A))$
Apply 6:
$(A \lor A)\Rightarrow (A\Rightarrow A)$
Apply 1: (or modus ponens?)
$A \lor A\Rightarrow A$
I think this is wrong because I don't think I can use 6 both to expand A and also to contract $A \lor B$ ... I think the rule would need a $\Leftrightarrow$ for that.
Thanks!
 A: There aren't a lot of ways to derive something about $\vee$; axiom 8 is about it.  From it (setting $B=C=A$), you can see that if we knew $A \Rightarrow A$, we could derive $(A\Rightarrow A)\Rightarrow (A\vee A \Rightarrow A)$, and from there derive $A\vee A \Rightarrow A$.  So how to derive $A \Rightarrow A$?  From axiom 2 (setting $C=A$) and axiom 1, we derive $(A\Rightarrow B)\Rightarrow(A\Rightarrow A)$.  Now we just need to derive $A\Rightarrow B$ for any old $B$.  There are several axioms of this form; any of axiom 1, axiom 6, or axiom 10 will work.  We may as well use axiom 1 again.  The upshot is that we can derive $A \vee A \Rightarrow A$ using only axioms (axiom schemas) 1, 2, and 8, together with modus ponens:
$$
\begin{array}{ l l l }
\text{a.} & (A \Rightarrow (B \Rightarrow A)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow A)) & \text{(specialization of axiom 2)} \\
\text{b.} & (A\Rightarrow B)\Rightarrow (A\Rightarrow A) & \text{(a. and axiom 1, using modus ponens)} \\
\text{c.} & A\Rightarrow (A\Rightarrow A) & \text{(specialization of axiom 1)} \\
\text{d.} & (A\Rightarrow (A\Rightarrow A)) \Rightarrow (A\Rightarrow A) & \text{(specialization of b.)} \\  
\text{e.} & A\Rightarrow A & \text{(c. and d., using modus ponens)} \\
\text{f.} & (A \Rightarrow A) \Rightarrow ((A \Rightarrow A) \Rightarrow (A \vee A \Rightarrow A)) & \text{(specialization of axiom 8)} \\
\text{g.} & (A \Rightarrow A) \Rightarrow (A \vee A \Rightarrow A) & \text{(e. and f., using modus ponens)} \\
\text{h.} & A \vee A \Rightarrow A & \text{(e. and g., using modus ponens)} \\
\end{array}
$$
