Metamath Proof Explorer

Theorem niabn

Description: Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994)

Ref Expression
Hypothesis niabn.1 
|- ph
Assertion niabn 
|- ( -. ps -> ( ( ch /\ ps ) <-> -. ph ) )

Proof

Step Hyp Ref Expression
1 niabn.1 
 |-  ph
2 simpr 
 |-  ( ( ch /\ ps ) -> ps )
3 1 pm2.24i 
 |-  ( -. ph -> ps )
4 2 3 pm5.21ni 
 |-  ( -. ps -> ( ( ch /\ ps ) <-> -. ph ) )