\fo\or提取
theorem fo_or_ext {x: set} (A B: wff x):
$ \fo x A \or \fo x B \imp \fo x (A \or B) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_collectl_or | (\fo x A \imp \fo x (A \or B)) \imp (\fo x B \imp \fo x (A \or B)) \imp \fo x A \or \fo x B \imp \fo x (A \or B) |
|
| 2 | intror_or | A \imp A \or B |
|
| 3 | 2 | imp_intro_fo | \fo x A \imp \fo x (A \or B) |
| 4 | 1, 3 | ax_mp | (\fo x B \imp \fo x (A \or B)) \imp \fo x A \or \fo x B \imp \fo x (A \or B) |
| 5 | introl_or | B \imp A \or B |
|
| 6 | 5 | imp_intro_fo | \fo x B \imp \fo x (A \or B) |
| 7 | 4, 6 | ax_mp | \fo x A \or \fo x B \imp \fo x (A \or B) |