Metamath Proof Explorer


Theorem nbn

Description: The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 3-Oct-2013)

Ref Expression
Hypothesis nbn.1 ¬ φ
Assertion nbn ¬ ψ ψ φ

Proof

Step Hyp Ref Expression
1 nbn.1 ¬ φ
2 bibif ¬ φ ψ φ ¬ ψ
3 1 2 ax-mp ψ φ ¬ ψ
4 3 bicomi ¬ ψ ψ φ