A theorem is simply a conclusion that can be proved from the empty set of premises. The most common technique for proving a theorem is to start with its denial as an assumption and construct a proof for it that discharges that assumption with RAA. If the theorem is a conditional, it may also be possible to prove it by assuming the antecedent, deducing the consequent, and using ->I. Here are some examples.
T1 (Identity): |- P->P
| 1 | (1) | P | A |
| (2) | P->P | 2 ->I (1) | |
This is about as short as a proof gets!
T2 (Excluded Middle): |- Pv~P
| 1 | (1) | ~(Pv~P) | A |
| 2 | (2) | P | A |
| 2 | (3) | Pv~P | 2 vI |
| 1 | (4) | ~P | 1,2 RAA (2) |
| 1 | (5) | Pv~P | 4 vI |
| (6) | Pv~P | 1,5 RAA (1) | |
T3 (Non-Contradiction): |- ~(P&~P)
| 1 | (1) | P&~P | A |
| 1 | (2) | P | 1 &E |
| 1 | (3) | ~P | 1 &E |
| (4) | ~(P&~P) | 2,3 RAA (1) |
T4 (Weakening): |- P->(Q->P)
| 1 | (1) | P | A |
| 2 | (2) | Q | A |
| 3 | (3) | ~P | A |
| 1 | (4) | P | 1,3 RAA (3) |
| 1 | (5) | Q->P | 4 ->I (2) |
| (6) | P->(Q->P) | 5 ->I (1) |
T5 (Paradox of Material Implication): |- (PvQ)v(QvP)
| 1 | (1) | ~((P->Q)v(Q->P)) | A |
| 2 | (2) | P | A |
| 3 | (3) | Q | A |
| 3 | (4) | P->Q | 3 ->I (2) |
| 3 | (5) | (P->Q)v(Q->P) | 4 vI |
| 1 | (6) | ~Q | 1,5 RAA (3) |
| 7 | (7) | Q | A |
| 8 | (8) | ~P | A |
| 1,7 | (9) | P | 6,7 RAA (8) |
| 1 | (10) | Q->P | 9 ->I (7) |
| 1 | (11) | (P->Q)v(Q->P) | 10 vI |
| (12) | (P->Q)v(Q->P) | 1,11 RAA(1) | |
T6 (Double Negation): |- P <-> ~~P
| 1 | (1) | P | A |
| 2 | (2) | ~P | A |
| 1 | (3) | ~~P | 1,2 RAA (2) |
| (4) | P->~~P | 3 ->I (1) | |
| (5) | ~~P->P | 4 Trans | |
| (6) | P<->~~P | 4,5 <->I |
T7: |- (P<->Q)<->(Q<->P)
With derived rules, this is very easy:
| 1 | (1) | P<->Q | A |
| 1 | (2) | Q<->P | 1 <-> Comm |
| (3) | (P<->Q)->(Q<->P) | 2 ->I (1) | |
| 4 | (4) | Q<->P | A |
| 4 | (5) | P<->Q | 4 <-> Comm |
| (6) | (Q<->P)->(P<->Q) | 5 ->I (4) | |
| (7) | (P<->Q)<->(Q<->P) | 3,6 <->I | |