This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ¬ 𝜑 ↔ ( 𝜑 → ⊥ ) )

Proof

Step	Hyp	Ref	Expression
1		fal	⊢ ¬ ⊥
2		mtt	⊢ ( ¬ ⊥ → ( ¬ 𝜑 ↔ ( 𝜑 → ⊥ ) ) )
3	1 2	ax-mp	⊢ ( ¬ 𝜑 ↔ ( 𝜑 → ⊥ ) )