\fo\imp引入左侧成\ex(右侧不出现)
theorem fo_imp_inslsto_ex_absrs (B: wff) {x: set} (A: wff x):
$ \fo x (A \imp B) \imp \ex x A \imp B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | (\fo x (A \imp B) \imp \neg B \imp \fo x \neg A) \imp ((\neg B \imp \fo x \neg A) \imp \neg \fo x \neg A \imp B) \imp \fo x (A \imp B) \imp \neg \fo x \neg A \imp B |
|
| 2 | imp_tran | (\fo x (A \imp B) \imp \fo x (\neg B \imp \neg A)) \imp (\fo x (\neg B \imp \neg A) \imp \neg B \imp \fo x \neg A) \imp \fo x (A \imp B) \imp \neg B \imp \fo x \neg A |
|
| 3 | imp_introrev_neg | (A \imp B) \imp \neg B \imp \neg A |
|
| 4 | 3 | imp_intro_fo | \fo x (A \imp B) \imp \fo x (\neg B \imp \neg A) |
| 5 | 2, 4 | ax_mp | (\fo x (\neg B \imp \neg A) \imp \neg B \imp \fo x \neg A) \imp \fo x (A \imp B) \imp \neg B \imp \fo x \neg A |
| 6 | fo_imp_insrs_absls | \fo x (\neg B \imp \neg A) \imp \neg B \imp \fo x \neg A |
|
| 7 | 5, 6 | ax_mp | \fo x (A \imp B) \imp \neg B \imp \fo x \neg A |
| 8 | 1, 7 | ax_mp | ((\neg B \imp \fo x \neg A) \imp \neg \fo x \neg A \imp B) \imp \fo x (A \imp B) \imp \neg \fo x \neg A \imp B |
| 9 | neg_imp_swap | (\neg B \imp \fo x \neg A) \imp \neg \fo x \neg A \imp B |
|
| 10 | 8, 9 | ax_mp | \fo x (A \imp B) \imp \neg \fo x \neg A \imp B |
| 11 | 10 | conv ex | \fo x (A \imp B) \imp \ex x A \imp B |