Metamath Proof Explorer

Theorem exmidne

Description: Excluded middle with equality and inequality. (Contributed by NM, 3-Feb-2012) (Proof shortened by Wolf Lammen, 17-Nov-2019)

Ref Expression
Assertion exmidne 
|- ( A = B \/ A =/= B )

Proof

Step Hyp Ref Expression
1 neqne 
 |-  ( -. A = B -> A =/= B )
2 1 orri 
 |-  ( A = B \/ A =/= B )