Theorem dfnot

Description: Given falsum F. , we can define the negation of a wff ph as the statement that F. follows from assuming ph . (Contributed by Mario Carneiro, 9-Feb-2017) (Proof shortened by Wolf Lammen, 21-Jul-2019)

	Ref	Expression
Assertion	dfnot	$$⊢\neg \phi \leftrightarrow \left(\phi \to \perp \right)$$

Proof

Step	Hyp	Ref	Expression
1		fal	$$⊢\neg \perp$$
2		mtt	$$⊢\neg \perp \to \left(\neg \phi \leftrightarrow \left(\phi \to \perp \right)\right)$$
3	1 2	ax-mp	$$⊢\neg \phi \leftrightarrow \left(\phi \to \perp \right)$$