Theorem sb_iff_ins ≪ | index | src | ≫

替换操作对等价的插入律

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

Step	Hyp	Ref	Expression
1		iff_comp	(\sb y x A \imp \sb y x B) \imp (\sb y x B \imp \sb y x A) \imp (\sb y x A \iff \sb y x B)
2	1	_hyp_null_complete	\sb y x (A \iff B) \imp (\sb y x A \imp \sb y x B) \imp (\sb y x B \imp \sb y x A) \imp (\sb y x A \iff \sb y x B)
3		imp_tran	(\sb y x (A \iff B) \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 \sb y x (A \iff B) \imp \sb y x A \imp \sb y x B
4		iff_decomp	(A \iff B) \imp A \imp B
5	4	imp_intro_sb	\sb y x (A \iff B) \imp \sb y x (A \imp B)
6	3, 5	ax_mp	(\sb y x (A \imp B) \imp \sb y x A \imp \sb y x B) \imp \sb y x (A \iff B) \imp \sb y x A \imp \sb y x B
7		sb_imp_ins	\sb y x (A \imp B) \imp \sb y x A \imp \sb y x B
8	6, 7	ax_mp	\sb y x (A \iff B) \imp \sb y x A \imp \sb y x B
9	8	_hyp_null_complete	\sb y x (A \iff B) \imp \sb y x (A \iff B) \imp \sb y x A \imp \sb y x B
10		_hyp_null_intro	\sb y x (A \iff B) \imp \sb y x (A \iff B)
11	9, 10	_hyp_mp	\sb y x (A \iff B) \imp \sb y x A \imp \sb y x B
12	2, 11	_hyp_mp	\sb y x (A \iff B) \imp (\sb y x B \imp \sb y x A) \imp (\sb y x A \iff \sb y x B)
13		imp_tran	(\sb y x (A \iff B) \imp \sb y x (B \imp A)) \imp (\sb y x (B \imp A) \imp \sb y x B \imp \sb y x A) \imp \sb y x (A \iff B) \imp \sb y x B \imp \sb y x A
14		iff_decompbwd	(A \iff B) \imp B \imp A
15	14	imp_intro_sb	\sb y x (A \iff B) \imp \sb y x (B \imp A)
16	13, 15	ax_mp	(\sb y x (B \imp A) \imp \sb y x B \imp \sb y x A) \imp \sb y x (A \iff B) \imp \sb y x B \imp \sb y x A
17		sb_imp_ins	\sb y x (B \imp A) \imp \sb y x B \imp \sb y x A
18	16, 17	ax_mp	\sb y x (A \iff B) \imp \sb y x B \imp \sb y x A
19	18	_hyp_null_complete	\sb y x (A \iff B) \imp \sb y x (A \iff B) \imp \sb y x B \imp \sb y x A
20	19, 10	_hyp_mp	\sb y x (A \iff B) \imp \sb y x B \imp \sb y x A
21	12, 20	_hyp_mp	\sb y x (A \iff B) \imp (\sb y x A \iff \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)