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