Theorem contradiction ≪ | index | src | ≫

矛盾律

theorem contradiction (A: wff): $ \neg (A \and \neg A) $;

Step	Hyp	Ref	Expression
1		negneg_intro	(A \imp \neg \neg A) \imp \neg \neg (A \imp \neg \neg A)
2		negneg_intro	A \imp \neg \neg A
3	1, 2	ax_mp	\neg \neg (A \imp \neg \neg A)
4	3	conv and	\neg (A \and \neg A)

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)