\fo\imp插入成\ex
theorem fo_imp_insto_ex {x: set} (A B: wff x):
$ \fo x (A \imp B) \imp \ex x A \imp \ex x B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | (\fo x (A \imp B) \imp \fo x \neg B \imp \fo x \neg A) \imp ((\fo x \neg B \imp \fo x \neg A) \imp \neg \fo x \neg A \imp \neg \fo x \neg B) \imp \fo x (A \imp B) \imp \neg \fo x \neg A \imp \neg \fo x \neg 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 \fo x \neg B \imp \fo x \neg A) \imp \fo x (A \imp B) \imp \fo x \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 \fo x \neg B \imp \fo x \neg A) \imp \fo x (A \imp B) \imp \fo x \neg B \imp \fo x \neg A |
| 6 | fo_imp_ins | \fo x (\neg B \imp \neg A) \imp \fo x \neg B \imp \fo x \neg A |
|
| 7 | 5, 6 | ax_mp | \fo x (A \imp B) \imp \fo x \neg B \imp \fo x \neg A |
| 8 | 1, 7 | ax_mp | ((\fo x \neg B \imp \fo x \neg A) \imp \neg \fo x \neg A \imp \neg \fo x \neg B) \imp \fo x (A \imp B) \imp \neg \fo x \neg A \imp \neg \fo x \neg B |
| 9 | imp_introrev_neg | (\fo x \neg B \imp \fo x \neg A) \imp \neg \fo x \neg A \imp \neg \fo x \neg B |
|
| 10 | 8, 9 | ax_mp | \fo x (A \imp B) \imp \neg \fo x \neg A \imp \neg \fo x \neg B |
| 11 | 10 | conv ex | \fo x (A \imp B) \imp \ex x A \imp \ex x B |