Theorem necomi 2689

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

Syntax hints:   =/= wne 2632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-cleq 2454  df-ne 2634

This theorem is referenced by:  nesymi  2692  nesymir  2693  0nep0  4587  xp01disj  7223  1sdom  7800  ltneii  9772  0ne1  10704  0ne2  10849  pnfnemnf  11445  mnfnepnf  11446  xmulpnf1  11588  fzprval  11884  hashneq0  12576  f1oun2prg  13047  geo2sum2  13978  fprodn0f  14093  xpscfn  15513  xpsc0  15514  xpsc1  15515  rescabs  15786  dmdprdpr  17730  dprdpr  17731  mgpress  17782  xpstopnlem1  20872  1sgm2ppw  24176  2sqlem11  24351  axlowdimlem13  25032  usgraexmpldifpr  25175  usgraexmplef  25176  constr3lem4  25423  ex-pss  25926  signswch  29498  bj-disjsn01  31587  bj-1upln0  31647  finxpreclem3  31829  funvtxval  39165  nnlog2ge0lt1  40649  logbpw2m1  40650  fllog2  40651  blennnelnn  40659  nnpw2blen  40663  blen1  40667  blen2  40668  blen1b  40671  blennnt2  40672  nnolog2flm1  40673  blennngt2o2  40675  blennn0e2  40677