\ex\and插入
theorem ex_and_ins {x: set} (A B: wff x):
$ \ex x (A \and B) \imp \ex x A \and \ex x B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_collectr_and | (\ex x (A \and B) \imp \ex x A) \imp (\ex x (A \and B) \imp \ex x B) \imp \ex x (A \and B) \imp \ex x A \and \ex x B |
|
| 2 | and_splitl | A \and B \imp A |
|
| 3 | 2 | imp_intro_ex | \ex x (A \and B) \imp \ex x A |
| 4 | 1, 3 | ax_mp | (\ex x (A \and B) \imp \ex x B) \imp \ex x (A \and B) \imp \ex x A \and \ex x B |
| 5 | and_splitr | A \and B \imp B |
|
| 6 | 5 | imp_intro_ex | \ex x (A \and B) \imp \ex x B |
| 7 | 4, 6 | ax_mp | \ex x (A \and B) \imp \ex x A \and \ex x B |