Theorem necomi 3053

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

Syntax hints:   ≠ wne 2999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-cleq 2818  df-ne 3000

This theorem is referenced by:  nesymi  3056  nesymir  3057  0nep0  5058  opthhausdorff  5203  xp01disj  7843  1sdom  8432  djuin  9057  pnfnemnf  10412  mnfnepnf  10413  ltneii  10469  0ne1  11422  0ne2  11565  xnn0n0n1ge2b  12251  xmulpnf1  12392  fzprval  12695  hashneq0  13445  f1oun2prg  14038  geo2sum2  14979  fprodn0f  15094  xpscfn  16572  xpsc0  16573  xpsc1  16574  rescabs  16845  dmdprdpr  18802  dprdpr  18803  mgpress  18854  cnfldfunALT  20119  xpstopnlem1  21983  2logb9irrALT  24938  sqrt2cxp2logb9e3  24939  1sgm2ppw  25338  2sqlem11  25567  axlowdimlem13  26253  usgrexmpldifpr  26555  usgrexmplef  26556  vdegp1ai  26834  vdegp1bi  26835  konigsbergiedgw  27627  konigsberglem2  27632  konigsberglem3  27633  ex-pss  27843  ex-hash  27868  signswch  31185  nosepnelem  32369  bj-disjsn01  33460  bj-1upln0  33519  finxpreclem3  33775  ovnsubadd2lem  41653  nnlog2ge0lt1  43207  logbpw2m1  43208  fllog2  43209  blennnelnn  43217  nnpw2blen  43221  blen1  43225  blen2  43226  blen1b  43229  blennnt2  43230  nnolog2flm1  43231  blennngt2o2  43233  blennn0e2  43235