Theorem _hyp_imp_intro_sb ≪ | index | src | ≫

imp_intro_sb的假设无关形式。

theorem _hyp_imp_intro_sb (G: wff) {x: set} (y: set) (A B: wff x):
  $ \nf x G $ >
  $ G \imp A \imp B $ >
  $ G \imp \sb y x A \imp \sb y x B $;

Step	Hyp	Ref	Expression
1		imp_tran	(G \imp \sb y x (A \imp B)) \imp (\sb y x (A \imp B) \imp \sb y x A \imp \sb y x B) \imp G \imp \sb y x A \imp \sb y x B
2		hyp g	\nf x G
3		hyp h	G \imp A \imp B
4	2, 3	_hyp_intro_sb	G \imp \sb y x (A \imp B)
5	1, 4	ax_mp	(\sb y x (A \imp B) \imp \sb y x A \imp \sb y x B) \imp G \imp \sb y x A \imp \sb y x B
6		sb_imp_ins	\sb y x (A \imp B) \imp \sb y x A \imp \sb y x B
7	5, 6	ax_mp	G \imp \sb y x A \imp \sb y x B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12)