Theorem necom 2983

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2930

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 2123  ax-ext 2705

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

This theorem is referenced by:  necomi  2984  necomd  2985  dfdif3  4068  0pss  4398  iftrueb  4489  disjtp2  4670  difprsn1  4753  difprsn2  4754  prproe  4858  fndmdifcom  6985  fvpr1g  7133  fvpr2g  7134  fvtp1  7138  fvtp2  7139  fvtp3  7140  fvtp1g  7141  fvtp2g  7142  fvtp3g  7143  dff14b  7214  f12dfv  7216  f13dfv  7217  orduniorsuc  7769  kmlem3  10054  kmlem4  10055  ac6num  10380  leltne  11212  nn0lt2  12546  xrleltne  13054  fzofzim  13619  elfznelfzo  13683  elfznelfzob  13684  fleqceilz  13768  hashdifpr  14332  hashgt12el  14339  hashgt12el2  14340  hashgt23el  14341  hash7g  14403  cshw0  14711  cshwn  14714  isprm2lem  16602  prm2orodd  16612  cshwsdisj  17020  sgrp2nmndlem5  18847  f1omvdconj  19368  pmtrprfv3  19376  pmtr3ncomlem1  19395  dmdprdd  19923  cnfldfunALT  21316  cnfldfunALTOLD  21329  xrsdsreclblem  21359  xrsdsreclb  21360  ordthaus  23309  hmphindis  23722  angpined  26777  nosgnn0  27607  noextendlt  27618  nosepne  27629  nosepdm  27633  nosupbnd2lem1  27664  noinfbnd2lem1  27679  noetasuplem4  27685  funvtxval0  29004  snstrvtxval  29026  snstriedgval  29027  nbgrsym  29352  nb3grprlem2  29370  nb3grpr  29371  cusgredg  29413  cplgr3v  29424  1egrvtxdg0  29501  usgr2pthlem  29752  usgr2pth0  29754  2pthdlem1  29919  clwlkclwwlklem2a4  29988  uhgr3cyclex  30173  eupth2lem3lem4  30222  frcond1  30257  frcond4  30261  frgr3v  30266  3vfriswmgr  30269  2pthfrgr  30275  3cyclfrgrrn1  30276  n4cyclfrgr  30282  frgrnbnb  30284  frgrwopreglem4a  30301  ch0pss  31436  pmtrprfv2  33068  esumcvgre  34115  bnj563  34766  cusgredgex2  35178  cvmsdisj  35325  fmlaomn0  35445  ex-sategoelel  35476  btwnouttr  36079  fscgr  36135  linecom  36205  linerflx2  36206  poimirlem25  37695  divrngidl  38078  lcvbr3  39132  opltn0  39299  atlltn0  39415  2dim  39579  ps-2  39587  islln3  39619  llnexatN  39630  4atlem11  39718  isline4N  39886  lhpex2leN  40122  cdleme48gfv  40646  60gcd7e1  42108  dvrelogpow2b  42171  aks4d1p1p4  42174  aks6d1c2p2  42222  fsuppind  42698  onov0suclim  43381  oenassex  43425  pr2eldif2  43662  pimxrneun  45600  icccncfext  45999  fourierdlem42  46261  icceuelpartlem  47549  ichnreuop  47586  paireqne  47625  oddprmALTV  47801  rrx2pnedifcoorneor  48831  rrx2linest  48857