Metamath Proof Explorer
Description: Inference associated with nesym . (Contributed by BJ, 7Jul2018)
(Proof shortened by Wolf Lammen, 25Nov2019)


Ref 
Expression 

Hypothesis 
nesymi.1 
$${\u22a2}{A}\ne {B}$$ 

Assertion 
nesymi 
$${\u22a2}\neg {B}={A}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nesymi.1 
$${\u22a2}{A}\ne {B}$$ 
2 
1

necomi 
$${\u22a2}{B}\ne {A}$$ 
3 
2

neii 
$${\u22a2}\neg {B}={A}$$ 