Theorem proof_by_absurd ≪ | index | src | ≫

归谬法

theorem proof_by_absurd (A: wff): $ (A \imp \false) \imp \neg A $;

Step	Hyp	Ref	Expression
1		iff_decomp	(A \imp \false \iff \neg A) \imp (A \imp \false) \imp \neg A
2		impfalse_eqv_negself	A \imp \false \iff \neg A
3	1, 2	ax_mp	(A \imp \false) \imp \neg A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)