vElim is just the formal proof rule that goes with proof by cases. Elim rules are for when you have a connective and need to reason from it, so vElim is for when you know a v and need to make an inference.
vElim works just like proof by cases, which means that we need a way of formally modelling temporary assumptions for the cases.
Think of it like this: each case is like a mini-proof inside the main proof, since we need to prove that the conclusion follows in each case. The temporary assumption is like the premise of the mini-proof.
To model this in our proof system, we will just create another proof, called a subproof, inside the main proof.
Let's see an example. Recall this equivalence:
PvQ ⇔ QvP
In order to prove this equivalence from left to right, we need to assume PvQ and show that QvP follows. So the formal proof will look something like this:
Since our premise is a v, we need to use vElim. In order to make subproofs for each case, just draw mini horizontal and vertical lines inside the main proof, like this:
Lines 2 and 3 are the subproof. Since line 2 is an assumption, like the original premise, it does not need justified. But line 3 occurs below the horizontal line, so it needs justified with a rule.
We've proven the conclusion in case 1, but we aren't done yet, because we need to prove the conclusion in every case. We need to end the first subproof and start a new one for case 2.
When we create case 2, it looks like this:
Notice how the final conclusion, on line 6, occurs outside the subproofs. That is key. We can't just show that the conclusion follows inside some subproof. If that were enough, we could have stopped at line 3. We need to show that the conclusion follows from just the original premise, without relying on additional temporary assumptions.
Also notice how we cite the last line: it is vElim because we are showing that QvP follows in the main proof from line 1. (And line 1 is a disjunction.)
In order for the vElim rule to work, you need the exact same sentence to appear at the end of each subproof, and then you write that same sentence out of the subproofs, on the main proof line. We call this "exporting" the sentence, since you move it out into the main proof.
The rule always requires you to cite three things: you must cite the disjunction you are using or "eliminating", and you need to cite the two subproofs you used for the cases. When you cite a subproof, you must use the dash "-", since you are not just citing an individual line. You are citing each subproof as a unit.
Your turn to try one. Here's the start of the proof of P from (P&Q)v(P&R):
Let's take it one part at a time.
Now your proof looks like this:
You've completed your first formal proof by cases, or vElim. Now you need lots of practice.
Remember when to use proof by cases: whenever you have a disjunction you need to reason from, proof by cases is how you do so.