I want to prove the law of excluded middle:
$A$
Thus $B ∨ ¬B$
under Copi's logic system.('A' means any premise. I want to derive the law of excluded middle from any premise, not means no premise) Copi system is constructed by 19 rules.
9 rules of inference: modus ponens(MP), modus tollens(MT), hypothetical syllogism(HS), disjunctive syllogism(DS), constructive dilemma(CD), simplification(Simp), conjunction(Conj), addition(Add), absorption(Abs)
10 rules of replacement: De Morgan's rule(DM), Commutativity(Com), Associativity(Assoc), Distrivution(Dist), Double Negation(DN), transposition(Trans), Material implication(Impl), Material equivalence(Equiv), exportation(Exp), Tautology(Taut)
I do not want to use conditional proof and indirect proof(reductio ad absurdum). Can I prove the above statement using only 19 rules?
\begin{array}{lll} 1. & A & Premise\\ 2. & A \lor \neg B& Add \ 1\\ 3. & \neg B \lor A& Comm \ 2\\ 4. & B \to A & Impl \ 3\\ 5. & B \to (B \land A) & Abs \ 4\\ 6. & \neg B \lor (B \land A) & Impl \ 5\\ 7. & (\neg B \lor B) \land (\neg B \lor A)& Dist \ 6\\ 8. & \neg B \lor B & Simp \ 7\\ 9. & B \lor \neg B & Comm \ 8\\ \end{array}