\ex\imp\fo提取成\fo
theorem ex_imp_fo_extto_fo {x: set} (A B: wff x):
$ (\ex x A \imp \fo x B) \imp \fo x (A \imp B) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | neg_imp_with_imp_mergel_imp | (\neg \ex x A \imp \fo x (A \imp B)) \imp (\fo x B \imp \fo x (A \imp B)) \imp (\ex x A \imp \fo x B) \imp \fo x (A \imp B) |
|
| 2 | iff_imp_tran_imp | (\neg \ex x A \iff \fo x \neg A) \imp (\fo x \neg A \imp \fo x (A \imp B)) \imp \neg \ex x A \imp \fo x (A \imp B) |
|
| 3 | iff_symm | (\fo x \neg A \iff \neg \ex x A) \imp (\neg \ex x A \iff \fo x \neg A) |
|
| 4 | foneg_eqv_negex | \fo x \neg A \iff \neg \ex x A |
|
| 5 | 3, 4 | ax_mp | \neg \ex x A \iff \fo x \neg A |
| 6 | 2, 5 | ax_mp | (\fo x \neg A \imp \fo x (A \imp B)) \imp \neg \ex x A \imp \fo x (A \imp B) |
| 7 | neg_elimintror_imp | \neg A \imp A \imp B |
|
| 8 | 7 | imp_intro_fo | \fo x \neg A \imp \fo x (A \imp B) |
| 9 | 6, 8 | ax_mp | \neg \ex x A \imp \fo x (A \imp B) |
| 10 | 1, 9 | ax_mp | (\fo x B \imp \fo x (A \imp B)) \imp (\ex x A \imp \fo x B) \imp \fo x (A \imp B) |
| 11 | introl_imp | B \imp A \imp B |
|
| 12 | 11 | imp_intro_fo | \fo x B \imp \fo x (A \imp B) |
| 13 | 10, 12 | ax_mp | (\ex x A \imp \fo x B) \imp \fo x (A \imp B) |