Metamath Proof Explorer
Description: Inference associated with dfne . (Contributed by BJ, 7Jul2018)


Ref 
Expression 

Hypothesis 
neir.1 
$${\u22a2}\neg {A}={B}$$ 

Assertion 
neir 
$${\u22a2}{A}\ne {B}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

neir.1 
$${\u22a2}\neg {A}={B}$$ 
2 

dfne 
$${\u22a2}{A}\ne {B}\leftrightarrow \neg {A}={B}$$ 
3 
1 2

mpbir 
$${\u22a2}{A}\ne {B}$$ 