\fo\or分配左侧(右侧不出现)
theorem fo_or_distls_nfrs {x: set} (A B: wff x):
$ \nf x B $ >
$ \fo x (A \or B) \iff \fo x A \or B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (\fo x (\neg A \imp B) \iff \ex x \neg A \imp B) \imp (\ex x \neg A \imp B \iff \neg \fo x A \imp B) \imp (\fo x (\neg A \imp B) \iff \neg \fo x A \imp B) |
|
| 2 | hyp n | \nf x B |
|
| 3 | 2 | fo_imp_distls_ex_nfrs | \fo x (\neg A \imp B) \iff \ex x \neg A \imp B |
| 4 | 1, 3 | ax_mp | (\ex x \neg A \imp B \iff \neg \fo x A \imp B) \imp (\fo x (\neg A \imp B) \iff \neg \fo x A \imp B) |
| 5 | iff_intror_imp | (\ex x \neg A \iff \neg \fo x A) \imp (\ex x \neg A \imp B \iff \neg \fo x A \imp B) |
|
| 6 | exneg_eqv_negfo | \ex x \neg A \iff \neg \fo x A |
|
| 7 | 5, 6 | ax_mp | \ex x \neg A \imp B \iff \neg \fo x A \imp B |
| 8 | 4, 7 | ax_mp | \fo x (\neg A \imp B) \iff \neg \fo x A \imp B |
| 9 | 8 | conv or | \fo x (A \or B) \iff \fo x A \or B |