\fo\and分配右侧(左侧不出现)
theorem fo_and_distrs_nfls {x: set} (A B: wff x):
$ \nf x A $ >
$ \fo x (A \and B) \iff A \and \fo x B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (\fo x (A \and B) \iff \fo x A \and \fo x B) \imp (\fo x A \and \fo x B \iff A \and \fo x B) \imp (\fo x (A \and B) \iff A \and \fo x B) |
|
| 2 | fo_and_dist | \fo x (A \and B) \iff \fo x A \and \fo x B |
|
| 3 | 1, 2 | ax_mp | (\fo x A \and \fo x B \iff A \and \fo x B) \imp (\fo x (A \and B) \iff A \and \fo x B) |
| 4 | iff_intror_and | (\fo x A \iff A) \imp (\fo x A \and \fo x B \iff A \and \fo x B) |
|
| 5 | iff_symm | (A \iff \fo x A) \imp (\fo x A \iff A) |
|
| 6 | hyp n | \nf x A |
|
| 7 | 6 | fo_alloc_nf | A \iff \fo x A |
| 8 | 5, 7 | ax_mp | \fo x A \iff A |
| 9 | 4, 8 | ax_mp | \fo x A \and \fo x B \iff A \and \fo x B |
| 10 | 3, 9 | ax_mp | \fo x (A \and B) \iff A \and \fo x B |