It will be needed the most complex derivation rule: the disjunction elimination. solved:

You already know the rules, so I just explain the way of thinking of a human who doesn't know natural deduction but can think a little:

We need to know that is always true. The expression from the left, , can be made true because of two causes:

- if it's true because is true, then is true.
- if it's true because is true, then both and are true, so is true because of .

Well, now we just need to translate all this to logical language, following the same order in which we thought that, and proceeding slowly.

We start proving one path, then the other, and finally we apply the disjunction elimination. To justify it we must write the line where the disjunction is in, and the two lines from inside each subdemonstration where we saw that both supposing one thing or supposing the other leads to the same result.

Notice that, even if we discovered that and that , it isn't necessary to use implication introduction to keep this written down.

The hardest thing in proof by cases is to decide which will be the expression to prove in both cases. It must be exactly the same in both cases!

Daniel Clemente Laboreo 2005-05-17