Theorem necom 2981

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  necomi  2982  necomd  2983  dfdif3  4067  0pss  4397  iftrueb  4488  disjtp2  4669  difprsn1  4752  difprsn2  4753  prproe  4857  fndmdifcom  6976  fvpr1g  7124  fvpr2g  7125  fvtp1  7129  fvtp2  7130  fvtp3  7131  fvtp1g  7132  fvtp2g  7133  fvtp3g  7134  dff14b  7205  f12dfv  7207  f13dfv  7208  orduniorsuc  7760  kmlem3  10044  kmlem4  10045  ac6num  10370  leltne  11202  nn0lt2  12536  xrleltne  13044  fzofzim  13609  elfznelfzo  13673  elfznelfzob  13674  fleqceilz  13758  hashdifpr  14322  hashgt12el  14329  hashgt12el2  14330  hashgt23el  14331  hash7g  14393  cshw0  14701  cshwn  14704  isprm2lem  16592  prm2orodd  16602  cshwsdisj  17010  sgrp2nmndlem5  18837  f1omvdconj  19359  pmtrprfv3  19367  pmtr3ncomlem1  19386  dmdprdd  19914  cnfldfunALT  21307  cnfldfunALTOLD  21320  xrsdsreclblem  21350  xrsdsreclb  21351  ordthaus  23300  hmphindis  23713  angpined  26768  nosgnn0  27598  noextendlt  27609  nosepne  27620  nosepdm  27624  nosupbnd2lem1  27655  noinfbnd2lem1  27670  noetasuplem4  27676  funvtxval0  28994  snstrvtxval  29016  snstriedgval  29017  nbgrsym  29342  nb3grprlem2  29360  nb3grpr  29361  cusgredg  29403  cplgr3v  29414  1egrvtxdg0  29491  usgr2pthlem  29742  usgr2pth0  29744  2pthdlem1  29909  clwlkclwwlklem2a4  29975  uhgr3cyclex  30160  eupth2lem3lem4  30209  frcond1  30244  frcond4  30248  frgr3v  30253  3vfriswmgr  30256  2pthfrgr  30262  3cyclfrgrrn1  30263  n4cyclfrgr  30269  frgrnbnb  30271  frgrwopreglem4a  30288  ch0pss  31423  pmtrprfv2  33055  esumcvgre  34102  bnj563  34753  cusgredgex2  35165  cvmsdisj  35312  fmlaomn0  35432  ex-sategoelel  35463  btwnouttr  36064  fscgr  36120  linecom  36190  linerflx2  36191  poimirlem25  37691  divrngidl  38074  lcvbr3  39068  opltn0  39235  atlltn0  39351  2dim  39515  ps-2  39523  islln3  39555  llnexatN  39566  4atlem11  39654  isline4N  39822  lhpex2leN  40058  cdleme48gfv  40582  60gcd7e1  42044  dvrelogpow2b  42107  aks4d1p1p4  42110  aks6d1c2p2  42158  fsuppind  42629  onov0suclim  43313  oenassex  43357  pr2eldif2  43594  pimxrneun  45532  icccncfext  45931  fourierdlem42  46193  icceuelpartlem  47472  ichnreuop  47509  paireqne  47548  oddprmALTV  47724  rrx2pnedifcoorneor  48754  rrx2linest  48780