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