Theorem necom 3040

Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)

Assertion

Ref	Expression
necom	⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Proof of Theorem necom

Step	Hyp	Ref	Expression
1		eqcom 2805	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2	1	necon3bii 3039	1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Syntax hints:   ↔ wb 209   ≠ wne 2987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  necomi  3041  necomd  3042  0pss  4352  disjtp2  4612  difprsn1  4693  difprsn2  4694  prproe  4798  fndmdifcom  6790  fvpr1  6929  fvpr2  6930  fvpr1g  6931  fvtp1  6934  fvtp2  6935  fvtp3  6936  fvtp1g  6937  fvtp2g  6938  fvtp3g  6939  dff14b  7007  f12dfv  7008  f13dfv  7009  orduniorsuc  7525  kmlem3  9563  kmlem4  9564  ac6num  9890  leltne  10719  nn0lt2  12033  xrleltne  12526  fzofzim  13079  elfznelfzo  13137  elfznelfzob  13138  fleqceilz  13217  hashdifpr  13772  hashgt12el  13779  hashgt12el2  13780  hashgt23el  13781  cshw0  14147  cshwn  14150  isprm2lem  16015  prm2orodd  16025  cshwsdisj  16424  sgrp2nmndlem5  18086  f1omvdconj  18566  pmtrprfv3  18574  pmtr3ncomlem1  18593  dmdprdd  19114  xrsdsreclblem  20137  xrsdsreclb  20138  ordthaus  21989  hmphindis  22402  angpined  25416  funvtxval0  26808  snstrvtxval  26830  snstriedgval  26831  nbgrsym  27153  nb3grprlem2  27171  nb3grpr  27172  cusgredg  27214  cplgr3v  27225  1egrvtxdg0  27301  usgr2pthlem  27552  usgr2pth0  27554  2pthdlem1  27716  clwlkclwwlklem2a4  27782  uhgr3cyclex  27967  eupth2lem3lem4  28016  frcond1  28051  frcond4  28055  frgr3v  28060  3vfriswmgr  28063  2pthfrgr  28069  3cyclfrgrrn1  28070  n4cyclfrgr  28076  frgrnbnb  28078  frgrwopreglem4a  28095  ch0pss  29228  pmtrprfv2  30782  esumcvgre  31460  bnj563  32124  cusgredgex2  32482  cvmsdisj  32630  fmlaomn0  32750  ex-sategoelel  32781  nosgnn0  33278  noextendlt  33289  nosepne  33298  nosepdm  33301  nosupbnd2lem1  33328  noetalem3  33332  btwnouttr  33598  fscgr  33654  linecom  33724  linerflx2  33725  poimirlem25  35082  divrngidl  35466  lcvbr3  36319  opltn0  36486  atlltn0  36602  2dim  36766  ps-2  36774  islln3  36806  llnexatN  36817  4atlem11  36905  isline4N  37073  lhpex2leN  37309  cdleme48gfv  37833  60gcd7e1  39293  fsuppind  39456  pr2eldif2  40254  icccncfext  42529  fourierdlem42  42791  icceuelpartlem  43952  ichnreuop  43989  paireqne  44028  oddprmALTV  44205  rrx2pnedifcoorneor  45130  rrx2linest  45156