Theorem imp_intro_sb ≪ | index | src | ≫

替换操作对蕴涵的引入律

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

Step	Hyp	Ref	Expression
1		sb_imp_ins	\sb y x (A \imp B) \imp \sb y x A \imp \sb y x B
2		hyp h	A \imp B
3	2	intro_sb	\sb y x (A \imp B)
4	1, 3	ax_mp	\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)