Theorem necom 2986

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2933

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  necomi  2987  necomd  2988  dfdif3  4071  0pss  4401  iftrueb  4494  disjtp2  4675  difprsn1  4758  difprsn2  4759  prproe  4863  fndmdifcom  6997  fvpr1g  7146  fvpr2g  7147  fvtp1  7151  fvtp2  7152  fvtp3  7153  fvtp1g  7154  fvtp2g  7155  fvtp3g  7156  dff14b  7227  f12dfv  7229  f13dfv  7230  orduniorsuc  7782  kmlem3  10075  kmlem4  10076  ac6num  10401  leltne  11234  nn0lt2  12567  xrleltne  13071  fzofzim  13637  elfznelfzo  13701  elfznelfzob  13702  fleqceilz  13786  hashdifpr  14350  hashgt12el  14357  hashgt12el2  14358  hashgt23el  14359  hash7g  14421  cshw0  14729  cshwn  14732  isprm2lem  16620  prm2orodd  16630  cshwsdisj  17038  sgrp2nmndlem5  18866  f1omvdconj  19387  pmtrprfv3  19395  pmtr3ncomlem1  19414  dmdprdd  19942  cnfldfunALT  21336  cnfldfunALTOLD  21349  xrsdsreclblem  21379  xrsdsreclb  21380  ordthaus  23340  hmphindis  23753  angpined  26808  nosgnn0  27638  noextendlt  27649  nosepne  27660  nosepdm  27664  nosupbnd2lem1  27695  noinfbnd2lem1  27710  noetasuplem4  27716  funvtxval0  29100  snstrvtxval  29122  snstriedgval  29123  nbgrsym  29448  nb3grprlem2  29466  nb3grpr  29467  cusgredg  29509  cplgr3v  29520  1egrvtxdg0  29597  usgr2pthlem  29848  usgr2pth0  29850  2pthdlem1  30015  clwlkclwwlklem2a4  30084  uhgr3cyclex  30269  eupth2lem3lem4  30318  frcond1  30353  frcond4  30357  frgr3v  30362  3vfriswmgr  30365  2pthfrgr  30371  3cyclfrgrrn1  30372  n4cyclfrgr  30378  frgrnbnb  30380  frgrwopreglem4a  30397  ch0pss  31532  pmtrprfv2  33181  esumcvgre  34268  bnj563  34919  cusgredgex2  35336  cvmsdisj  35483  fmlaomn0  35603  ex-sategoelel  35634  btwnouttr  36237  fscgr  36293  linecom  36363  linerflx2  36364  poimirlem25  37893  divrngidl  38276  lcvbr3  39396  opltn0  39563  atlltn0  39679  2dim  39843  ps-2  39851  islln3  39883  llnexatN  39894  4atlem11  39982  isline4N  40150  lhpex2leN  40386  cdleme48gfv  40910  60gcd7e1  42372  dvrelogpow2b  42435  aks4d1p1p4  42438  aks6d1c2p2  42486  fsuppind  42945  onov0suclim  43628  oenassex  43672  pr2eldif2  43908  pimxrneun  45843  icccncfext  46242  fourierdlem42  46504  icceuelpartlem  47792  ichnreuop  47829  paireqne  47868  oddprmALTV  48044  rrx2pnedifcoorneor  49073  rrx2linest  49099