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
|- ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) )

Proof

Step Hyp Ref Expression
1 pm5.501
 |-  ( -. ph -> ( -. ps <-> ( -. ph <-> -. ps ) ) )
2 notbi
 |-  ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) )
3 1 2 bitr4di
 |-  ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) )