How to prove Disjunction Elimination rule of inference I've looked at the tableau proofs of many rules of inference (double-negation, disjunction is commutative, modus tollendo ponens, and others), and they all seem to use the so-called "or-elimination" (Disjunction Elimination) rule:
$$(P\vdash R), (Q\vdash R), (P \lor Q) \vdash R$$
(If $P\implies R$ and $Q\implies R$, and either $P$ or $Q$ (or both) are true, then $R$ must be true.)
It's often called the "proof by cases" rule, it makes sense, and I've seen the principle used in many mathematical proofs.
I'm trying to figure out how to logically prove this rule (using other rules of inference and/or replacement), however the proof offered is self-reliant! Is this an axiom?
(There's also the Constructive Dilemma rule, which looks like a more generalized version of Disjunction Elimination. Maybe the proof of D.E. depends on C.D.? or maybe C.D. is an extension of D.E.?)

The rules of Disjunction Elimination and Constructive dilemma are interchangable.
You can proof Disjunction Elimination from Constructive Dilemma and
You can proof Constructive Dilemma from Disjunction Elimination.
So whichever you have you can prove the other.
Your second question is Disjunction Elimination an axiom?
In a strict logical sense axioms are formulas that are treated as self-evidently true.
Rules of inference are not formulas so in the strict sense they cannot be axioms.
But seeing in it in a more relaxed way , they are treated as self-evidently true so you could call it a metalogical axiom or something like it.  
