Metamath Proof Explorer

Theorem nesymir

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

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

Proof

Step Hyp Ref Expression
1 nesymir.1 
 |-  -. A = B
2 1 neir 
 |-  A =/= B
3 2 necomi 
 |-  B =/= A