Theorem imp_and_extr_or ≪ | index | src | ≫

\imp\and右提取\or

theorem imp_and_extr_or (A B C: wff):
  $ (A \imp C) \and (B \imp C) \imp A \or B \imp C $;

Step	Hyp	Ref	Expression
1		imp_nested_assemb_and	((A \imp C) \imp (B \imp C) \imp A \or B \imp C) \imp (A \imp C) \and (B \imp C) \imp A \or B \imp C
2		imp_mergel_neg_imp	(A \imp C) \imp (B \imp C) \imp (\neg A \imp B) \imp C
3	2	_hyp_null_complete	(A \imp C) \and (B \imp C) \imp (A \imp C) \imp (B \imp C) \imp (\neg A \imp B) \imp C
4		_hyp_null_intro	(A \imp C) \imp A \imp C
5	4	_hyp_complete	(A \imp C) \and (B \imp C) \imp A \imp C
6	3, 5	_hyp_mp	(A \imp C) \and (B \imp C) \imp (B \imp C) \imp (\neg A \imp B) \imp C
7		_hyp_intro	(A \imp C) \and (B \imp C) \imp B \imp C
8	6, 7	_hyp_mp	(A \imp C) \and (B \imp C) \imp (\neg A \imp B) \imp C
9	8	conv or	(A \imp C) \and (B \imp C) \imp A \or B \imp C
10	9	_hyp_rm	(A \imp C) \imp (B \imp C) \imp A \or B \imp C
11	1, 10	ax_mp	(A \imp C) \and (B \imp C) \imp A \or B \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)