\imp左侧引入\ex(右侧无关)
theorem imp_introls_ex_nfrs {x: set} (A B: wff x):
$ \nf x B $ >
$ A \imp B $ >
$ \ex x A \imp B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | neg_imp_swap | (\neg B \imp \fo x \neg A) \imp \neg \fo x \neg A \imp B |
|
| 2 | 1 | conv ex | (\neg B \imp \fo x \neg A) \imp \ex x A \imp B |
| 3 | hyp n | \nf x B |
|
| 4 | 3 | _nf_clos_neg | \nf x \neg B |
| 5 | imp_introrev_neg | (A \imp B) \imp \neg B \imp \neg A |
|
| 6 | hyp h | A \imp B |
|
| 7 | 5, 6 | ax_mp | \neg B \imp \neg A |
| 8 | 4, 7 | imp_intrors_fo_nfls | \neg B \imp \fo x \neg A |
| 9 | 2, 8 | ax_mp | \ex x A \imp B |