Description: Law of noncontradiction with equality and inequality. (Contributed by NM, 3Feb2012) (Proof shortened by Wolf Lammen, 21Dec2019)
Ref  Expression  

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

1  fal   . F. 

2  eqneqall   ( A = B > ( A =/= B > F. ) ) 

3  2  imp   ( ( A = B /\ A =/= B ) > F. ) 
4  1 3  mto   . ( A = B /\ A =/= B ) 