Theorem imp_and_extl_or ≪ | index | src | ≫

\imp\and左提取\or

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

Step	Hyp	Ref	Expression
1		imp_tran	((A \imp B) \and (A \imp C) \imp A \imp B \and C) \imp ((A \imp B \and C) \imp A \imp B \or C) \imp (A \imp B) \and (A \imp C) \imp A \imp B \or C
2		imp_and_extl	(A \imp B) \and (A \imp C) \imp A \imp B \and C
3	1, 2	ax_mp	((A \imp B \and C) \imp A \imp B \or C) \imp (A \imp B) \and (A \imp C) \imp A \imp B \or C
4		imp_introl_imp	(B \and C \imp B \or C) \imp (A \imp B \and C) \imp A \imp B \or C
5		and_to_or	B \and C \imp B \or C
6	4, 5	ax_mp	(A \imp B \and C) \imp A \imp B \or C
7	3, 6	ax_mp	(A \imp B) \and (A \imp C) \imp A \imp B \or C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)