Theorem imp_and_extr ≪ | index | src | ≫

\imp\and右提取

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

Step	Hyp	Ref	Expression
1		imp_introlsr_and	((A \imp C) \imp A \and B \imp C) \imp (A \imp C) \and (B \imp C) \imp A \and B \imp C
2		imp_introlsr_and	(A \imp C) \imp A \and B \imp C
3	1, 2	ax_mp	(A \imp C) \and (B \imp C) \imp A \and B \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)