\fo对\iff插入
theorem fo_iff_ins {x: set} (A B: wff x):
$ \fo x (A \iff B) \imp (\fo x A \iff \fo x B) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_collectr_and | (\fo x (A \iff B) \imp \fo x A \imp \fo x B) \imp (\fo x (A \iff B) \imp \fo x B \imp \fo x A) \imp \fo x (A \iff B) \imp (\fo x A \imp \fo x B) \and (\fo x B \imp \fo x A) |
|
| 2 | imp_tran | (\fo x (A \iff B) \imp \fo x (A \imp B)) \imp (\fo x (A \imp B) \imp \fo x A \imp \fo x B) \imp \fo x (A \iff B) \imp \fo x A \imp \fo x B |
|
| 3 | iff_decomp | (A \iff B) \imp A \imp B |
|
| 4 | 3 | imp_intro_fo | \fo x (A \iff B) \imp \fo x (A \imp B) |
| 5 | 2, 4 | ax_mp | (\fo x (A \imp B) \imp \fo x A \imp \fo x B) \imp \fo x (A \iff B) \imp \fo x A \imp \fo x B |
| 6 | fo_imp_ins | \fo x (A \imp B) \imp \fo x A \imp \fo x B |
|
| 7 | 5, 6 | ax_mp | \fo x (A \iff B) \imp \fo x A \imp \fo x B |
| 8 | 1, 7 | ax_mp | (\fo x (A \iff B) \imp \fo x B \imp \fo x A) \imp \fo x (A \iff B) \imp (\fo x A \imp \fo x B) \and (\fo x B \imp \fo x A) |
| 9 | imp_tran | (\fo x (A \iff B) \imp \fo x (B \imp A)) \imp (\fo x (B \imp A) \imp \fo x B \imp \fo x A) \imp \fo x (A \iff B) \imp \fo x B \imp \fo x A |
|
| 10 | iff_decompbwd | (A \iff B) \imp B \imp A |
|
| 11 | 10 | imp_intro_fo | \fo x (A \iff B) \imp \fo x (B \imp A) |
| 12 | 9, 11 | ax_mp | (\fo x (B \imp A) \imp \fo x B \imp \fo x A) \imp \fo x (A \iff B) \imp \fo x B \imp \fo x A |
| 13 | fo_imp_ins | \fo x (B \imp A) \imp \fo x B \imp \fo x A |
|
| 14 | 12, 13 | ax_mp | \fo x (A \iff B) \imp \fo x B \imp \fo x A |
| 15 | 8, 14 | ax_mp | \fo x (A \iff B) \imp (\fo x A \imp \fo x B) \and (\fo x B \imp \fo x A) |
| 16 | 15 | conv iff | \fo x (A \iff B) \imp (\fo x A \iff \fo x B) |