| |
|
| │(A → B) ∧ (B → C) | 1 |
| ├─ | |
| 1 Ext | │A → B | 4 |
| 1 Ext | │B → C | 5,10 |
| │ | |
| ││A ∨ B | 3 |
| │├─ | |
| │││A | (4) |
| ││├─ | |
| 4 MPP | │││B | (5) |
| 5 MPP | │││C | |
| 6 Adj | │││B ∧ C | X,(7) |
| │││● | |
| ││├─ | |
| 7 QED | │││B ∧ C | 3 |
| ││ | |
| │││B | (9),(10) |
| ││├─ | |
| ││││● | |
| │││├─ | |
| 9 QED | ││││B | 8 |
| │││ | |
| 10 MPP | ││││C | (11) |
| ││││● | |
| │││├─ | |
| 11 QED | ││││C | 8 |
| ││├─ | |
| 8 Cnj | │││B ∧ C | 3 |
| │├─ | |
| 3 PC | ││B ∧ C | 2 |
| ├─ | |
| 2 CP | │(A ∨ B) → (B ∧ C) | |
|
|
| │(A ∨ B) → (B ∧ C) | 4,10 |
| ├─ | |
| │││A | (3) |
| ││├─ | |
| 3 Wk | │││A ∨ B | X,(4) |
| 4 MPP | │││B ∧ C | 5 |
| 5 Ext | │││B | (6) |
| 5 Ext | │││C | |
| │││● | |
| ││├─ | |
| 6 QED | │││B | 2 |
| │├─ | |
| 2 CP | ││A → B | 1 |
| │ | |
| │││B | (11) |
| ││├─ | |
| ││││¬ C | (9) |
| │││├─ | |
| 9 Wk | ││││¬ (B ∧ C) | (10) |
| 10 MTT | ││││¬ (A ∨ B) | (12) |
| 11 Wk | ││││A ∨ B | (12) |
| ││││● | |
| │││├─ | |
| 12 Nc | ││││ ⊥ | 8 |
| ││├─ | |
| 8 IP | │││C | 7 |
| │├─ | |
| 7 CP | ││B → C | 1 |
| ├─ | |
| 1 Cnj | │(A → B) ∧ (B → C) | |
|