iff_intro_ex的假设无关形式（不可引用）
theorem _hyp_iff_intro_ex {x: set} (G A B: wff x):
$ \nf x G $ >
$ G \imp (A \iff B) $ >
$ G \imp (\ex x A \iff \ex x B) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | (G \imp \fo x (A \iff B)) \imp (\fo x (A \iff B) \imp (\ex x A \iff \ex x B)) \imp G \imp (\ex x A \iff \ex x B) |
|
| 2 | hyp g | \nf x G |
|
| 3 | hyp h | G \imp (A \iff B) |
|
| 4 | 2, 3 | _hyp_intro_fo | G \imp \fo x (A \iff B) |
| 5 | 1, 4 | ax_mp | (\fo x (A \iff B) \imp (\ex x A \iff \ex x B)) \imp G \imp (\ex x A \iff \ex x B) |
| 6 | fo_iff_insto_ex | \fo x (A \iff B) \imp (\ex x A \iff \ex x B) |
|
| 7 | 5, 6 | ax_mp | G \imp (\ex x A \iff \ex x B) |