Theorem necomi 3005

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 3004	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	mpbi 233	1 ⊢ 𝐵 ≠ 𝐴

Syntax hints:   ≠ wne 2951

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 2729

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

This theorem is referenced by:  nesymi  3008  nesymir  3009  0nep0  5230  opthhausdorff  5380  xp01disj  8136  xp01disjl  8137  1sdom  8772  djuexb  9384  djuin  9393  pnfnemnf  10747  mnfnepnf  10748  ltneii  10804  0ne1  11758  0ne2  11894  xnn0n0n1ge2b  12580  xmulpnf1  12721  fzprval  13030  hashneq0  13788  f1oun2prg  14339  geo2sum2  15291  fnpr2o  16902  fvpr0o  16904  fvpr1o  16905  rescabs  17176  symgvalstruct  18606  dmdprdpr  19253  dprdpr  19254  mgpress  19332  cnfldfunALT  20193  xpstopnlem1  22523  2logb9irrALT  25497  sqrt2cxp2logb9e3  25498  1sgm2ppw  25897  2sqlem11  26126  axlowdimlem13  26861  usgrexmpldifpr  27161  usgrexmplef  27162  vdegp1ai  27439  vdegp1bi  27440  konigsbergiedgw  28146  konigsberglem2  28151  konigsberglem3  28152  ex-pss  28326  ex-hash  28351  signswch  32072  nogesgn1ores  33475  nosepnelem  33480  noinfbnd1lem3  33526  noinfbnd1lem5  33528  noinfbnd2lem1  33531  bj-disjsn01  34704  bj-1upln0  34761  finxpreclem3  35125  remul01  39932  sn-0tie0  39963  flt0  40011  mnuprdlem2  41399  ovnsubadd2lem  43695  nnlog2ge0lt1  45404  logbpw2m1  45405  fllog2  45406  blennnelnn  45414  nnpw2blen  45418  blen1  45422  blen2  45423  blen1b  45426  blennnt2  45427  nnolog2flm1  45428  blennngt2o2  45430  blennn0e2  45432  inlinecirc02plem  45624