Metamath Proof Explorer

Theorem nbn3

Description: Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006)

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

Proof

Step Hyp Ref Expression
1 nbn3.1 
 |-  ph
2 1 notnoti 
 |-  -. -. ph
3 2 nbn 
 |-  ( -. ps <-> ( ps <-> -. ph ) )