Theorem necomi 3001

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

Syntax hints:   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  nesymi  3004  nesymir  3005  0nep0  5376  opthhausdorff  5536  xp01disj  8547  xp01disjl  8548  enpr2d  9115  snnen2o  9300  rex2dom  9309  1sdomOLD  9312  djuexb  9978  djuin  9987  pnfnemnf  11345  mnfnepnf  11346  ltneii  11403  0ne1  12364  0ne2  12500  xnn0n0n1ge2b  13194  xmulpnf1  13336  fzprval  13645  fvf1tp  13840  hashneq0  14413  f1oun2prg  14966  geo2sum2  15922  ressplusg  17349  ressmulr  17366  fnpr2o  17617  fvpr0o  17619  fvpr1o  17620  rescabs  17896  rescabsOLD  17897  odubas  18361  symgvalstruct  19438  symgvalstructOLD  19439  dmdprdpr  20093  dprdpr  20094  mgpress  20176  mgpressOLD  20177  rmodislmod  20950  sralem  21198  srasca  21206  sratset  21211  srads  21214  cnfldfun  21401  cnfldfunALT  21402  cnfldfunOLD  21414  cnfldfunALTOLD  21415  zlmbas  21552  zlmplusg  21554  zlmmulr  21556  zlmsca  21558  znbas2  21578  znadd  21580  znmul  21582  opsrbas  22092  opsrplusg  22094  opsrmulr  22096  opsrvsca  22098  opsrsca  22100  xpstopnlem1  23838  tuslem  24296  setsmsbas  24506  tngbas  24676  tngplusg  24678  tngmulr  24681  tngsca  24683  tngvsca  24685  tngip  24687  2logb9irrALT  26859  sqrt2cxp2logb9e3  26860  1sgm2ppw  27262  2sqlem11  27491  nogesgn1ores  27737  nosepnelem  27742  noinfbnd1lem3  27788  noinfbnd1lem5  27790  noinfbnd2lem1  27793  ttgval  28901  ttgbas  28905  ttgplusg  28907  ttgvsca  28910  ttgds  28912  cchhllem  28919  axlowdimlem13  28987  usgrexmpldifpr  29293  usgrexmplef  29294  vdegp1ai  29572  vdegp1bi  29573  konigsbergiedgw  30280  konigsberglem2  30285  konigsberglem3  30286  ex-pss  30460  ex-hash  30485  resvbas  33324  resvplusg  33326  resvmulr  33330  2sqr3minply  33738  signswch  34538  bj-disjsn01  36918  bj-1upln0  36975  finxpreclem3  37359  hlhilsbase  41897  hlhilsplus  41899  hlhilsmul  41901  aks6d1c7lem1  42137  ine1  42303  remul01  42383  sn-0tie0  42415  flt0  42592  mnuprdlem2  44242  ovnsubadd2lem  46566  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb2  47848  nnlog2ge0lt1  48300  logbpw2m1  48301  fllog2  48302  blennnelnn  48310  nnpw2blen  48314  blen1  48318  blen2  48319  blen1b  48322  blennnt2  48323  nnolog2flm1  48324  blennngt2o2  48326  blennn0e2  48328  inlinecirc02plem  48520