Theorem necomi 2713

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

Syntax hints:   =/= wne 2638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ne 2640

This theorem is referenced by:  nesymi  2716  nesymir  2718  0nep0  4608  xp01disj  7148  1sdom  7724  ltneii  9700  0ne1  10610  0ne2  10754  pnfnemnf  11337  mnfnepnf  11338  xmulpnf1  11477  fzprval  11751  hashneq0  12416  f1oun2prg  12847  geo2sum2  13665  xpscfn  14938  xpsc0  14939  xpsc1  14940  rescabs  15184  dmdprdpr  17077  dprdpr  17078  mgpress  17131  xpstopnlem1  20288  1sgm2ppw  23453  2sqlem11  23628  axlowdimlem13  24235  usgraexmpldifpr  24378  usgraexmpl  24379  constr3lem4  24625  ex-pss  25127  signswch  28496  fprodn0f  31548  bj-disjsn01  34389  bj-1upln0  34450