Metamath Proof Explorer

Theorem bibif

Description: Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007) (Proof shortened by Wolf Lammen, 28-Jan-2013)

Ref Expression
Assertion bibif 
|- ( -. ps -> ( ( ph <-> ps ) <-> -. ph ) )

Proof

Step Hyp Ref Expression
1 nbn2 
 |-  ( -. ps -> ( -. ph <-> ( ps <-> ph ) ) )
2 bicom 
 |-  ( ( ps <-> ph ) <-> ( ph <-> ps ) )
3 1 2 bitr2di 
 |-  ( -. ps -> ( ( ph <-> ps ) <-> -. ph ) )