Theorem necomi 2692

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 2691	. 2 |- ( A =/= B <-> B =/= A )
3	1, 2	mpbi 208	1 |- B =/= A

Syntax hints:   =/= wne 2604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-cleq 2434  df-ne 2606

This theorem is referenced by:  0nep0  4460  xp01disj  6932  1sdom  7511  ltneii  9483  0ne1  10385  0ne2  10529  pnfnemnf  11093  mnfnepnf  11094  xmulpnf1  11233  fzprval  11513  hashneq0  12128  hash2pwpr  12178  f1oun2prg  12523  geo2sum2  13330  xpscfn  14493  xpsc0  14494  xpsc1  14495  rescabs  14742  dmdprdpr  16538  dprdpr  16539  mgpress  16592  xpstopnlem1  19341  1sgm2ppw  22498  2sqlem11  22673  axlowdimlem13  23135  usgraexmpldifpr  23253  usgraexmpl  23254  constr3lem4  23468  ex-pss  23570  resvvsca  26238  eulerpartlemgf  26692  sgnnbi  26858  signswch  26892  wepwsolem  29319  refsum2cnlem1  29684  bj-disjsn01  32171  bj-1upln0  32232