Theorem necom 2985

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2932

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 2708

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

This theorem is referenced by:  necomi  2986  necomd  2987  dfdif3  4057  0pss  4387  iftrueb  4479  disjtp2  4660  difprsn1  4745  difprsn2  4746  prproe  4848  fndmdifcom  6995  fvpr1g  7145  fvpr2g  7146  fvtp1  7150  fvtp2  7151  fvtp3  7152  fvtp1g  7153  fvtp2g  7154  fvtp3g  7155  dff14b  7226  f12dfv  7228  f13dfv  7229  orduniorsuc  7781  kmlem3  10075  kmlem4  10076  ac6num  10401  leltne  11235  nn0lt2  12592  xrleltne  13096  fzofzim  13664  elfznelfzo  13728  elfznelfzob  13729  fleqceilz  13813  hashdifpr  14377  hashgt12el  14384  hashgt12el2  14385  hashgt23el  14386  hash7g  14448  cshw0  14756  cshwn  14759  isprm2lem  16650  prm2orodd  16660  cshwsdisj  17069  sgrp2nmndlem5  18900  f1omvdconj  19421  pmtrprfv3  19429  pmtr3ncomlem1  19448  dmdprdd  19976  cnfldfunALT  21367  xrsdsreclblem  21393  xrsdsreclb  21394  ordthaus  23349  hmphindis  23762  angpined  26794  nosgnn0  27622  noextendlt  27633  nosepne  27644  nosepdm  27648  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetasuplem4  27700  funvtxval0  29084  snstrvtxval  29106  snstriedgval  29107  nbgrsym  29432  nb3grprlem2  29450  nb3grpr  29451  cusgredg  29493  cplgr3v  29504  1egrvtxdg0  29580  usgr2pthlem  29831  usgr2pth0  29833  2pthdlem1  29998  clwlkclwwlklem2a4  30067  uhgr3cyclex  30252  eupth2lem3lem4  30301  frcond1  30336  frcond4  30340  frgr3v  30345  3vfriswmgr  30348  2pthfrgr  30354  3cyclfrgrrn1  30355  n4cyclfrgr  30361  frgrnbnb  30363  frgrwopreglem4a  30380  ch0pss  31516  pmtrprfv2  33149  esumcvgre  34235  bnj563  34886  cusgredgex2  35305  cvmsdisj  35452  fmlaomn0  35572  ex-sategoelel  35603  btwnouttr  36206  fscgr  36262  linecom  36332  linerflx2  36333  mh-inf3f1  36723  poimirlem25  37966  divrngidl  38349  lcvbr3  39469  opltn0  39636  atlltn0  39752  2dim  39916  ps-2  39924  islln3  39956  llnexatN  39967  4atlem11  40055  isline4N  40223  lhpex2leN  40459  cdleme48gfv  40983  60gcd7e1  42444  dvrelogpow2b  42507  aks4d1p1p4  42510  aks6d1c2p2  42558  fsuppind  43023  onov0suclim  43702  oenassex  43746  pr2eldif2  43982  pimxrneun  45916  icccncfext  46315  fourierdlem42  46577  icceuelpartlem  47895  ichnreuop  47932  paireqne  47971  oddprmALTV  48163  rrx2pnedifcoorneor  49192  rrx2linest  49218