Metamath Proof Explorer

Theorem ninba

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

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

Proof

Step Hyp Ref Expression
1 ninba.1 
 |-  ph
2 1 niabn 
 |-  ( -. ps -> ( ( ch /\ ps ) <-> -. ph ) )
3 2 bicomd 
 |-  ( -. ps -> ( -. ph <-> ( ch /\ ps ) ) )