\ex\and\fo提取成\ex
theorem ex_and_fo_extto_ex {x: set} (A B: wff x):
$ \ex x A \and \fo x B \imp \ex x (A \and B) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_iff_tran_imp | (\ex x A \and \fo x B \imp \ex x (B \and A)) \imp (\ex x (B \and A) \iff \ex x (A \and B)) \imp \ex x A \and \fo x B \imp \ex x (A \and B) |
|
| 2 | iff_imp_tran_imp | (\ex x A \and \fo x B \iff \fo x B \and \ex x A) \imp (\fo x B \and \ex x A \imp \ex x (B \and A)) \imp \ex x A \and \fo x B \imp \ex x (B \and A) |
|
| 3 | and_comm | \ex x A \and \fo x B \iff \fo x B \and \ex x A |
|
| 4 | 2, 3 | ax_mp | (\fo x B \and \ex x A \imp \ex x (B \and A)) \imp \ex x A \and \fo x B \imp \ex x (B \and A) |
| 5 | fo_and_ex_extto_ex | \fo x B \and \ex x A \imp \ex x (B \and A) |
|
| 6 | 4, 5 | ax_mp | \ex x A \and \fo x B \imp \ex x (B \and A) |
| 7 | 1, 6 | ax_mp | (\ex x (B \and A) \iff \ex x (A \and B)) \imp \ex x A \and \fo x B \imp \ex x (A \and B) |
| 8 | and_comm | B \and A \iff A \and B |
|
| 9 | 8 | iff_intro_ex | \ex x (B \and A) \iff \ex x (A \and B) |
| 10 | 7, 9 | ax_mp | \ex x A \and \fo x B \imp \ex x (A \and B) |