I've been toying with a system of inference rules for propositional logic. I can use the system to prove theorems; but my question is, can I use the system to obtain new inference rules?

Here are the details. We begin with 5 inference rules, and 0 axioms.

(1) *Proof by contradiction.* We can open a proof/subproof by assuming $\neg A$. If we obtain a contradiction, we may close the proof/subproof and deduce $A$.

(2) *Double Negation Elimination.* $$\neg\neg A \vdash A$$

(3) *Conjunction Elimination.* $$A \wedge B \vdash A,\quad A \wedge B \vdash B$$

(4) *De Morgan's Principles.*

$$\neg(A \wedge B) \vdash \neg A \vee \neg B,\quad \neg(A \vee B) \vdash \neg A \wedge \neg B$$

(5) *[Don't Know What To Call This]*

$$(\neg A \vee \neg B), A \vdash \neg B,\quad (\neg A \vee \neg B), B \vdash \neg A$$

Now it seems to me that I can prove a lot using just these rules; I'm guessing the logic is complete. For a simple example, lets prove $\neg(A \wedge B) \vee (B \wedge A).$ Assume not.

Then by De Morgan, we get $\neg\neg(A \wedge B) \wedge \neg(B \wedge A)$.

Using both versions of rule (3), we obtain

* $\neg\neg(A \wedge B)$
* $\neg(B \wedge A)$

which (by 2) becomes

* $A \wedge B$
* $\neg(B \wedge A)$

which using both versions of rule (3) again, becomes

* $A$
* $B$
* $\neg(B \wedge A)$

which (thank you for the correction, Doug) becomes 

* $A$
* $B$
* $\neg B \vee \neg A.$

Finally, using rule (5), from $B$ and $\neg B \vee \neg A$ we deduce $\neg A$.

Since both $A$ and $\neg A$ are written down, we're done!

Okay, so we've proved the theorem $\neg(A \wedge B) \vee (B \wedge A).$ But, I'd like to view this as a new rule of inference rather than a theorem. Am I allowed to deduce that $A \wedge B \vdash B \wedge A$ is an admissible rule of inference? *In general, how does one deduce a new rule of inference?*

For instance, is it a general principle that if we have a theorem of the general form $\neg \Gamma \vee \Delta$, then it follows that $\Gamma \vdash \Delta$ is an admissible rule of inference?

Is the converse true?

Similarly, suppose we want to demonstrate that a rule of the form $\Gamma, \Gamma' \vdash \Delta$ is admissible. Is it sufficient to begin the game with $\Gamma$ and $\Gamma'$ written down, and deduce $\Delta$? If so, why? I'm having difficulty organizing my thoughts on the issue.