Metamath Proof Explorer

Theorem notbii

Description: Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993) (Proof shortened by Wolf Lammen, 19-May-2013)

Ref Expression
Hypothesis notbii.1 
|- ( ph <-> ps )
Assertion notbii 
|- ( -. ph <-> -. ps )

Proof

Step Hyp Ref Expression
1 notbii.1 
 |-  ( ph <-> ps )
2 notbi 
 |-  ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) )
3 1 2 mpbi 
 |-  ( -. ph <-> -. ps )