Metamath Proof Explorer


Theorem nbn2

Description: The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006) (Proof shortened by Wolf Lammen, 28-Jan-2013)

Ref Expression
Assertion nbn2 ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( 𝜑𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 pm5.501 ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( ¬ 𝜑 ↔ ¬ 𝜓 ) ) )
2 notbi ( ( 𝜑𝜓 ) ↔ ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3 1 2 bitr4di ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( 𝜑𝜓 ) ) )