Theorem necomi 3041

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

Hypothesis

Ref	Expression
necomi.1	⊢ 𝐴 ≠ 𝐵

Assertion

Ref	Expression
necomi	⊢ 𝐵 ≠ 𝐴

Proof of Theorem necomi

Step	Hyp	Ref	Expression
1		necomi.1	. 2 ⊢ 𝐴 ≠ 𝐵
2		necom 3040	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	mpbi 233	1 ⊢ 𝐵 ≠ 𝐴

Syntax hints:   ≠ wne 2987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  nesymi  3044  nesymir  3045  0nep0  5223  opthhausdorff  5372  xp01disj  8103  xp01disjl  8104  1sdom  8705  djuexb  9322  djuin  9331  pnfnemnf  10685  mnfnepnf  10686  ltneii  10742  0ne1  11696  0ne2  11832  xnn0n0n1ge2b  12514  xmulpnf1  12655  fzprval  12963  hashneq0  13721  f1oun2prg  14270  geo2sum2  15222  fnpr2o  16822  fvpr0o  16824  fvpr1o  16825  rescabs  17095  symgvalstruct  18517  dmdprdpr  19164  dprdpr  19165  mgpress  19243  cnfldfunALT  20104  xpstopnlem1  22414  2logb9irrALT  25384  sqrt2cxp2logb9e3  25385  1sgm2ppw  25784  2sqlem11  26013  axlowdimlem13  26748  usgrexmpldifpr  27048  usgrexmplef  27049  vdegp1ai  27326  vdegp1bi  27327  konigsbergiedgw  28033  konigsberglem2  28038  konigsberglem3  28039  ex-pss  28213  ex-hash  28238  signswch  31941  nosepnelem  33297  bj-disjsn01  34388  bj-1upln0  34445  finxpreclem3  34810  remul01  39545  sn-0tie0  39576  mnuprdlem2  40981  ovnsubadd2lem  43284  nnlog2ge0lt1  44980  logbpw2m1  44981  fllog2  44982  blennnelnn  44990  nnpw2blen  44994  blen1  44998  blen2  44999  blen1b  45002  blennnt2  45003  nnolog2flm1  45004  blennngt2o2  45006  blennn0e2  45008  inlinecirc02plem  45200