Theorem necomi 2836

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

Syntax hints:   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  nesymi  2839  nesymir  2840  0nep0  4762  xp01disj  7463  1sdom  8048  pnfnemnf  9973  mnfnepnf  9974  ltneii  10029  0ne1  10965  0ne2  11116  xnn0n0n1ge2b  11841  xmulpnf1  11976  fzprval  12271  hashneq0  13016  f1oun2prg  13512  geo2sum2  14444  fprodn0f  14561  xpscfn  16042  xpsc0  16043  xpsc1  16044  rescabs  16316  dmdprdpr  18271  dprdpr  18272  mgpress  18323  xpstopnlem1  21422  1sgm2ppw  24725  2sqlem11  24954  axlowdimlem13  25634  usgraexmpldifpr  25928  usgraexmplef  25929  constr3lem4  26175  ex-pss  26677  ex-hash  26702  signswch  29964  bj-disjsn01  32130  bj-1upln0  32190  finxpreclem3  32406  ovnsubadd2lem  39535  vdegp1ai-av  40752  vdegp1bi-av  40753  konigsbergiedgw  41416  konigsberglem2  41423  konigsberglem3  41424  nnlog2ge0lt1  42158  logbpw2m1  42159  fllog2  42160  blennnelnn  42168  nnpw2blen  42172  blen1  42176  blen2  42177  blen1b  42180  blennnt2  42181  nnolog2flm1  42182  blennngt2o2  42184  blennn0e2  42186