Theorem and_updr ≪ | index | src | ≫

\and右更新

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

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

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)