Theorem necomi 2694

Description: Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)

Hypothesis

Ref	Expression
necomi.1	|- A =/= B

Assertion

Ref	Expression
necomi	|- B =/= A

Proof of Theorem necomi

Step	Hyp	Ref	Expression
1		necomi.1	. 2 |- A =/= B
2		necom 2693	. 2 |- ( A =/= B <-> B =/= A )
3	1, 2	mpbi 208	1 |- B =/= A

Syntax hints:   =/= wne 2606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-cleq 2436  df-ne 2608

This theorem is referenced by:  0nep0  4463  xp01disj  6936  1sdom  7515  ltneii  9487  0ne1  10389  0ne2  10533  pnfnemnf  11097  mnfnepnf  11098  xmulpnf1  11237  fzprval  11517  hashneq0  12132  hash2pwpr  12182  f1oun2prg  12527  geo2sum2  13334  xpscfn  14497  xpsc0  14498  xpsc1  14499  rescabs  14746  dmdprdpr  16548  dprdpr  16549  mgpress  16602  xpstopnlem1  19382  1sgm2ppw  22539  2sqlem11  22714  axlowdimlem13  23200  usgraexmpldifpr  23318  usgraexmpl  23319  constr3lem4  23533  ex-pss  23635  resvvsca  26302  eulerpartlemgf  26762  sgnnbi  26928  signswch  26962  wepwsolem  29394  refsum2cnlem1  29759  bj-disjsn01  32441  bj-1upln0  32502