Description: Excluded middle with equality and inequality. (Contributed by NM, 3Feb2012) (Proof shortened by Wolf Lammen, 17Nov2019)
Ref  Expression  

Assertion  exmidne   ( A = B \/ A =/= B ) 
Step  Hyp  Ref  Expression 

1  neqne   ( . A = B > A =/= B ) 

2  1  orri   ( A = B \/ A =/= B ) 