Theorem necomi 2848

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

Syntax hints:   ≠ wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  nesymi  2851  nesymir  2852  0nep0  4836  xp01disj  7576  1sdom  8163  pnfnemnf  10094  mnfnepnf  10095  ltneii  10150  0ne1  11088  0ne2  11239  xnn0n0n1ge2b  11965  xmulpnf1  12104  fzprval  12401  hashneq0  13155  f1oun2prg  13662  geo2sum2  14605  fprodn0f  14722  xpscfn  16219  xpsc0  16220  xpsc1  16221  rescabs  16493  dmdprdpr  18448  dprdpr  18449  mgpress  18500  cnfldfunALT  19759  xpstopnlem1  21612  1sgm2ppw  24925  2sqlem11  25154  axlowdimlem13  25834  usgrexmpldifpr  26150  usgrexmplef  26151  vdegp1ai  26432  vdegp1bi  26433  konigsbergiedgw  27108  konigsberglem2  27115  konigsberglem3  27116  ex-pss  27285  ex-hash  27310  signswch  30638  nosepnelem  31830  bj-disjsn01  32937  bj-1upln0  32997  finxpreclem3  33230  ovnsubadd2lem  40859  nnlog2ge0lt1  42360  logbpw2m1  42361  fllog2  42362  blennnelnn  42370  nnpw2blen  42374  blen1  42378  blen2  42379  blen1b  42382  blennnt2  42383  nnolog2flm1  42384  blennngt2o2  42386  blennn0e2  42388