Theorem necomi 3068

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

Syntax hints:   ≠ wne 3014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812  df-ne 3015

This theorem is referenced by:  nesymi  3071  nesymir  3072  0nep0  5249  opthhausdorff  5398  xp01disj  8112  xp01disjl  8113  1sdom  8713  djuexb  9330  djuin  9339  pnfnemnf  10688  mnfnepnf  10689  ltneii  10745  0ne1  11700  0ne2  11836  xnn0n0n1ge2b  12518  xmulpnf1  12659  fzprval  12960  hashneq0  13717  f1oun2prg  14271  geo2sum2  15222  fnpr2o  16822  fvpr0o  16824  fvpr1o  16825  rescabs  17095  symgvalstruct  18517  dmdprdpr  19163  dprdpr  19164  mgpress  19242  cnfldfunALT  20550  xpstopnlem1  22409  2logb9irrALT  25368  sqrt2cxp2logb9e3  25369  1sgm2ppw  25768  2sqlem11  25997  axlowdimlem13  26732  usgrexmpldifpr  27032  usgrexmplef  27033  vdegp1ai  27310  vdegp1bi  27311  konigsbergiedgw  28019  konigsberglem2  28024  konigsberglem3  28025  ex-pss  28199  ex-hash  28224  signswch  31824  nosepnelem  33177  bj-disjsn01  34257  bj-1upln0  34314  finxpreclem3  34666  remul01  39228  mnuprdlem2  40600  ovnsubadd2lem  42918  nnlog2ge0lt1  44617  logbpw2m1  44618  fllog2  44619  blennnelnn  44627  nnpw2blen  44631  blen1  44635  blen2  44636  blen1b  44639  blennnt2  44640  nnolog2flm1  44641  blennngt2o2  44643  blennn0e2  44645  inlinecirc02plem  44764