\fo\and\ex提取成\ex
theorem fo_and_ex_extto_ex {x: set} (A B: wff x):
$ \fo x A \and \ex x B \imp \ex x (A \and B) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_nested_assemb_and | (\fo x A \imp \ex x B \imp \ex x (A \and B)) \imp \fo x A \and \ex x B \imp \ex x (A \and B) |
|
| 2 | imp_tran | (\fo x A \imp \fo x (B \imp A \and B)) \imp (\fo x (B \imp A \and B) \imp \ex x B \imp \ex x (A \and B)) \imp \fo x A \imp \ex x B \imp \ex x (A \and B) |
|
| 3 | and_comp | A \imp B \imp A \and B |
|
| 4 | 3 | imp_intro_fo | \fo x A \imp \fo x (B \imp A \and B) |
| 5 | 2, 4 | ax_mp | (\fo x (B \imp A \and B) \imp \ex x B \imp \ex x (A \and B)) \imp \fo x A \imp \ex x B \imp \ex x (A \and B) |
| 6 | fo_imp_insto_ex | \fo x (B \imp A \and B) \imp \ex x B \imp \ex x (A \and B) |
|
| 7 | 5, 6 | ax_mp | \fo x A \imp \ex x B \imp \ex x (A \and B) |
| 8 | 1, 7 | ax_mp | \fo x A \and \ex x B \imp \ex x (A \and B) |