Theorem imp_collectr_and ≪ | index | src | ≫

\imp右聚集\and

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

Step	Hyp	Ref	Expression
1		and_imp_break_nested	((A \imp B) \and (A \imp C) \imp A \imp B \and C) \imp (A \imp B) \imp (A \imp C) \imp A \imp B \and 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) \imp (A \imp C) \imp A \imp B \and C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)