T1   |- P->P       T2   |- P v ~P       T3   |- ~(P & ~P)       T4   |- P->(Q->P)       T5   |- (P->Q) v (Q->P)       T6   |- P <-> ~~P       T7   |- (P <-> Q) <-> (Q <-> P)       T8   |- ~(P <-> Q) <-> (~P <-> Q)       T9   |- ((P->Q)->P)->P       T10   |- (P->Q) v (Q->R)       T11   |- (P <-> Q) <-> (~ P <-> ~Q)       T12    |- (~P->Q) & (R->Q) <-> (P->R)->Q       T13   |- P <-> P & P       T14   |- P <-> P v P       T15   |- (P <-> Q) & (R <-> S)->((P->R) <-> (Q->S))       T16   |- (P <-> Q) & (R <-> S)->(P & R <-> Q & S)       T17   |- (P <-> Q) & (R <-> S)->(P v R <-> Q v S)       T18   |- (P <-> Q) & (R <-> S)->((P <-> R) <-> (Q <-> S))       T19   |- (P <-> Q)-> ((R->P) <-> (R->Q)) & ((P->R) <-> (Q->R))       T20   |- (P <-> Q)->(R & P <-> R & Q)       T21   |- (P <-> Q)->(R v P <-> R v Q)       T22   |- (P <-> Q)->((R <-> P) <-> (R <-> Q))       T23   |- P & (Q <-> R)->(P & Q <-> R)       T24   |- P->(Q->R) <-> ((P->Q)->(P->R))       T25   |- P->(Q->R) <-> Q->(P->R)       T26   |- P->(P->Q) <-> P->Q       T27   |- (P->Q)->Q <-> (Q->P)->P       T28   |- P->~Q <-> Q->~P       T29   |- ~P -> P <-> P       T30   |- (P & Q) v (R & S) <-> ((P v R) & (P v S)) & ((Q v R) & (Q v S))       T31   |- (P v Q) & (R v S) <-> ((P & R) v (P & S)) v ((Q & R) v (Q & S))       T32   |- (P->Q) & (R->S) <-> ((~P & ~R) v (~P & S)) v ((Q & ~R) v (Q & S))       T33   |- (P v ~P) & Q <-> Q       T34   |- (P & ~P) v Q <-> Q       T35   |- P v (~P & Q) <-> P v Q       T36   |- P & (~P v Q) <-> P & Q       T37   |- P <-> P v (P & Q)       T38   |- P <-> P & (P v Q)       T39   |- (P->Q & R) -> (P & Q <-> P & R)