From a subproof ¬α |- [ ]
Infer α in that subproof
1. F <-> (M ^ P)
2. M
3. P
4. Therefore, F
| 1a. | ¬FM | // premise, from 1 |
| 1b. | ¬FP | // premise, from 1 |
| 1c. | ¬M¬PF | // premise, from 1 |
| 2. | M | // premise, from 2 |
| 3. | P | // premise, from 3 |
| * 4. | ¬F | // temporary premise, from 4 |
| * 5. | ¬M¬PF | // send 1c |
| * 6. | ¬M¬P | // 1c, 4, Resolution |
| * 7. | M | // send 2 |
| * 8. | ¬P | // 6, 7, Resolution |
| * 9. | P | // send 3 |
| *10. | [ ] | // 8, 9, Resolution |
| *11. | F | // 4, 10, ¬Elimination |
| 12. | F | // return 11 |