Theorem necom 2998

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 205   ≠ wne 2944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-ne 2945

This theorem is referenced by:  necomi  2999  necomd  3000  0pss  4379  disjtp2  4653  difprsn1  4734  difprsn2  4735  prproe  4838  fndmdifcom  6929  fvpr1g  7071  fvpr2g  7072  fvpr1OLD  7075  fvpr2OLD  7077  fvtp1  7079  fvtp2  7080  fvtp3  7081  fvtp1g  7082  fvtp2g  7083  fvtp3g  7084  dff14b  7153  f12dfv  7154  f13dfv  7155  orduniorsuc  7686  kmlem3  9917  kmlem4  9918  ac6num  10244  leltne  11073  nn0lt2  12392  xrleltne  12888  fzofzim  13443  elfznelfzo  13501  elfznelfzob  13502  fleqceilz  13583  hashdifpr  14139  hashgt12el  14146  hashgt12el2  14147  hashgt23el  14148  cshw0  14516  cshwn  14519  isprm2lem  16395  prm2orodd  16405  cshwsdisj  16809  sgrp2nmndlem5  18577  f1omvdconj  19063  pmtrprfv3  19071  pmtr3ncomlem1  19090  dmdprdd  19611  cnfldfunALT  20619  xrsdsreclblem  20653  xrsdsreclb  20654  ordthaus  22544  hmphindis  22957  angpined  25989  funvtxval0  27394  snstrvtxval  27416  snstriedgval  27417  nbgrsym  27739  nb3grprlem2  27757  nb3grpr  27758  cusgredg  27800  cplgr3v  27811  1egrvtxdg0  27887  usgr2pthlem  28140  usgr2pth0  28142  2pthdlem1  28304  clwlkclwwlklem2a4  28370  uhgr3cyclex  28555  eupth2lem3lem4  28604  frcond1  28639  frcond4  28643  frgr3v  28648  3vfriswmgr  28651  2pthfrgr  28657  3cyclfrgrrn1  28658  n4cyclfrgr  28664  frgrnbnb  28666  frgrwopreglem4a  28683  ch0pss  29816  pmtrprfv2  31366  esumcvgre  32068  bnj563  32732  cusgredgex2  33093  cvmsdisj  33241  fmlaomn0  33361  ex-sategoelel  33392  nosgnn0  33870  noextendlt  33881  nosepne  33892  nosepdm  33896  nosupbnd2lem1  33927  noinfbnd2lem1  33942  noetasuplem4  33948  btwnouttr  34335  fscgr  34391  linecom  34461  linerflx2  34462  poimirlem25  35811  divrngidl  36195  lcvbr3  37044  opltn0  37211  atlltn0  37327  2dim  37491  ps-2  37499  islln3  37531  llnexatN  37542  4atlem11  37630  isline4N  37798  lhpex2leN  38034  cdleme48gfv  38558  60gcd7e1  40020  dvrelogpow2b  40083  aks4d1p1p4  40086  fsuppind  40286  pr2eldif2  41169  icccncfext  43435  fourierdlem42  43697  icceuelpartlem  44898  ichnreuop  44935  paireqne  44974  oddprmALTV  45150  rrx2pnedifcoorneor  46073  rrx2linest  46099