Theorem necomi 2737

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

Syntax hints:   =/= wne 2662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664

This theorem is referenced by:  nesymi  2740  nesymir  2742  0nep0  4618  xp01disj  7146  1sdom  7722  ltneii  9697  0ne1  10603  0ne2  10747  pnfnemnf  11326  mnfnepnf  11327  xmulpnf1  11466  fzprval  11740  hashneq0  12402  hash2pwpr  12485  f1oun2prg  12828  geo2sum2  13646  xpscfn  14814  xpsc0  14815  xpsc1  14816  rescabs  15063  dmdprdpr  16900  dprdpr  16901  mgpress  16954  xpstopnlem1  20073  1sgm2ppw  23231  2sqlem11  23406  axlowdimlem13  23961  usgraexmpldifpr  24104  usgraexmpl  24105  constr3lem4  24351  ex-pss  24854  resvvsca  27515  eulerpartlemgf  27986  sgnnbi  28152  signswch  28186  wepwsolem  30619  refsum2cnlem1  31018  fourierdlem60  31495  fourierdlem61  31496  bj-disjsn01  33605  bj-1upln0  33666