Number | Statement | Lines Used | Reason |
---|
:. | | P -> (~P -> (Q <-> (R v S))) | | |
| 1 | P | | ACP |
| 2 | ~~P | 1 | DN |
| 3 | ~~P v (P -> (Q <-> (R v S))) | 2 | Add |
| 4 | ~P -> (P -> (Q <-> (R v S))) | 3 | MI |
| 5 | (~P & P) -> (Q <-> (R v S)) | 4 | Exp |
| 6 | (P & ~P) -> (Q <-> (R v S)) | 5 | Comm |
| 7 | P -> (~P -> (Q <-> (R v S))) | 6 | Exp |
8 | | P -> {P -> (~P -> (Q <-> (R v S)))} | 1-7 | CP |
9 | | (P & P) -> (~P -> (Q <-> (R v S))) | 8 | Exp |
10 | | P -> (~P -> (Q <-> (R v S))) | 9 | Taut |