Any proof by LEM+disjunction elimination may be rewritten as a proof by Reduction to Absurdity. Take the following structure:
| P v ~P TautCon (LEM) | |_ P Assume | | : | | Q derived somehow | + | |_ ~P Assume | | : | | Q derived somehow | Q Disjunction Elimination
Q may be derived from both
~P, we may rewrite this to give the required contradiction.
| |_ ~Q Assume | | |_ P Assume | | | : | | | Q derived | | | # Negation Elimination | | ~P Negation Introduction | | : | | Q derived | | # Negation Elimination | ~~Q Negation Introduction | Q Double Negation Elimination