Metamath Proof Explorer

Theorem nesymi

Description: Inference associated with nesym . (Contributed by BJ, 7-Jul-2018) (Proof shortened by Wolf Lammen, 25-Nov-2019)

Ref Expression
Hypothesis nesymi.1 
|- A =/= B
Assertion nesymi 
|- -. B = A

Proof

Step Hyp Ref Expression
1 nesymi.1 
 |-  A =/= B
2 1 necomi 
 |-  B =/= A
3 2 neii 
 |-  -. B = A