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 ) )