Theorem fo_imp_insrs_absls ≪ | index | src | ≫

\fo\imp插入右侧(左侧不出现)

theorem fo_imp_insrs_absls (A: wff) {x: set} (B: wff x):
  $ \fo x (A \imp B) \imp A \imp \fo x B $;

Step	Hyp	Ref	Expression
1		imp_tran	(A \imp \fo x A) \imp (\fo x A \imp \fo x B) \imp A \imp \fo x B
2	1	_hyp_null_complete	\fo x (A \imp B) \imp (A \imp \fo x A) \imp (\fo x A \imp \fo x B) \imp A \imp \fo x B
3		fo_intro_abs	A \imp \fo x A
4	3	_hyp_null_complete	\fo x (A \imp B) \imp A \imp \fo x A
5	2, 4	_hyp_mp	\fo x (A \imp B) \imp (\fo x A \imp \fo x B) \imp A \imp \fo x B
6		fo_imp_ins	\fo x (A \imp B) \imp \fo x A \imp \fo x B
7	6	_hyp_null_complete	\fo x (A \imp B) \imp \fo x (A \imp B) \imp \fo x A \imp \fo x B
8		_hyp_null_intro	\fo x (A \imp B) \imp \fo x (A \imp B)
9	7, 8	_hyp_mp	\fo x (A \imp B) \imp \fo x A \imp \fo x B
10	5, 9	_hyp_mp	\fo x (A \imp B) \imp A \imp \fo x B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_4, ax_5)