Metamath Proof Explorer

Theorem bj-nimni

Description: Inference associated with bj-nimn . (Contributed by BJ, 19-Mar-2020)

Ref Expression
Hypothesis bj-nimni.1 
|- ph
Assertion bj-nimni 
|- -. ( ph -> -. ph )

Proof

Step Hyp Ref Expression
1 bj-nimni.1 
 |-  ph
2 bj-nimn 
 |-  ( ph -> -. ( ph -> -. ph ) )
3 1 2 ax-mp 
 |-  -. ( ph -> -. ph )