Theorem neeq1 3003

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)

Assertion

Ref	Expression
neeq1	⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	neeq1d 3000	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  pm13.18  3022  pm13.181  3023  nelrdva  3711  psseq1  4090  n0snor2el  4833  0inp0  5359  nnullss  5467  opeqex  5503  friOLD  5643  frsn  5773  xp11  6195  limeq  6396  tz6.12i  6934  fveqressseq  7099  funopsn  7168  fprg  7175  tpres  7221  f1dom3el3dif  7289  f1ounsn  7292  f1prex  7304  isofrlem  7360  resf1extb  7956  f1oweALT  7997  frxp  8151  xpord2lem  8167  poxp2  8168  frxp2  8169  xpord2indlem  8172  xpord3lem  8174  frxp3  8176  xpord3inddlem  8179  suppimacnv  8199  elqsn0  8826  frfi  9321  fiint  9366  fiintOLD  9367  marypha1lem  9473  frmin  9789  eldju2ndl  9964  dfac8alem  10069  dfac8clem  10072  aceq3lem  10160  dfac5lem3  10165  dfac5lem4  10166  dfac5lem4OLD  10168  dfac5  10169  dfac2b  10171  dfac9  10177  kmlem1  10191  kmlem12  10202  kmlem14  10204  fin2i  10335  isfin2-2  10359  fin23lem21  10379  fin1a2lem10  10449  axcc2lem  10476  dominf  10485  ac5b  10518  zornn0g  10545  axdclem  10559  dominfac  10613  elwina  10726  elina  10727  iswun  10744  rankcf  10817  axrrecex  11203  elimne0  11251  1re  11261  recex  11895  xnn0nemnf  12610  uzn0  12895  qreccl  13011  xrnemnf  13159  xrnepnf  13160  xnn0n0n1ge2b  13174  fztpval  13626  expcl2lem  14114  hashnemnf  14383  hashneq0  14403  hashge2el2difr  14520  hashdmpropge2  14522  relexp1g  15065  ntrivcvgn0  15934  ntrivcvgmullem  15937  fprodntriv  15978  divalglem7  16436  divalg  16440  gcdcllem1  16536  gcdcllem3  16538  pcpre1  16880  pcqmul  16891  pcqcl  16894  prmgaplem3  17091  prmgaplem4  17092  xpsfrnel  17607  mreintcl  17638  isdrs  18347  isipodrs  18582  sgrp2rid2ex  18940  frgpuptinv  19789  isnzr2  20518  nrhmzr  20537  isdrngrd  20766  isdrngrdOLD  20768  psgnodpmr  21608  lindfrn  21841  dmatelnd  22502  dmatmul  22503  mdetdiaglem  22604  mdetunilem1  22618  fvmptnn04ifa  22856  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  fiinopn  22907  hausnei  23336  dfconn2  23427  2ndcdisj  23464  regr1lem2  23748  isfbas  23837  ioorinv  25611  ioorcl  25612  vitalilem2  25644  vitalilem3  25645  vitali  25648  itg1climres  25749  mbfi1fseqlem4  25753  dvferm1lem  26022  dvferm2lem  26024  isuc1p  26180  ismon1p  26182  ply1remlem  26204  plydivlem4  26338  aannenlem1  26370  aannenlem2  26371  lgsne0  27379  lgsqr  27395  nolesgn2ores  27717  nogesgn1ores  27719  nosepdmlem  27728  nosupbnd1lem3  27755  nosupbnd1lem5  27757  nosupbnd2lem1  27760  noinfbnd1lem3  27770  noinfbnd1lem5  27772  noinfbnd2lem1  27775  axtg5seg  28473  axtgupdim2  28479  axtgeucl  28480  axlowdim1  28974  lpvtx  29085  umgrnloopv  29123  usgrnloopvALT  29218  umgrvad2edg  29230  cusgrfilem2  29474  pthdlem2lem  29787  iswwlks  29856  iswwlksnx  29860  2pthdlem1  29950  isclwwlk  30003  3pthdlem1  30183  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  eupth2lem2  30238  eupth2lem3lem4  30250  eupth2lem3lem6  30252  3cyclfrgrrn1  30304  4cycl2vnunb  30309  frgrreg  30413  norm1exi  31269  shintcl  31349  chintcl  31351  chne0  31513  elspansn2  31586  eigre  31854  eigorth  31857  kbpj  31975  superpos  32373  hatomic  32379  isprmidl  33466  ismxidl  33490  ssmxidllem  33501  ssmxidl  33502  constrconj  33786  2sqr3minply  33791  zarcmplem  33880  xrge0iifhom  33936  xrge0iif1  33937  esumpr2  34068  sibfof  34342  signswn0  34575  signswch  34576  signstfvneq0  34587  axtgupdim2ALTV  34683  bnj168  34744  bnj970  34961  bnj1154  35013  umgracycusgr  35159  cusgracyclt3v  35161  subfacp1lem1  35184  erdszelem8  35203  indispconn  35239  cvmsss2  35279  nepss  35718  elwlim  35824  dfrdg4  35952  fvray  36142  linedegen  36144  fvline  36145  hilbert1.1  36155  rankeq1o  36172  unblimceq0lem  36507  knoppndvlem21  36533  poimirlem1  37628  poimirlem17  37644  poimirlem20  37647  poimirlem32  37659  itg2addnclem3  37680  neificl  37760  isdrngo3  37966  ispridl  38041  ismaxidl  38047  islshp  38980  lsatn0  39000  lshpset2N  39120  atlex  39317  hlsuprexch  39383  3dimlem1  39460  llni2  39514  lplni2  39539  2llnjN  39569  lvoli2  39583  2lplnj  39622  islinei  39742  lnatexN  39781  llnexchb2  39871  lhpmatb  40033  cdleme40m  40469  cdlemftr3  40567  cdlemk28-3  40910  cdlemk35s  40939  cdlemk39s  40941  cdlemk42  40943  metakunt30  42235  nnn1suc  42301  dnnumch1  43056  aomclem3  43068  aomclem8  43073  dfac11  43074  dfacbasgrp  43120  dfsucon  43536  ax6e2ndeq  44579  ax6e2ndeqVD  44929  relpfrlem  44974  fnchoice  45034  fiiuncl  45070  disjrnmpt2  45193  idlimc  45641  limcperiod  45643  limclner  45666  cnrefiisp  45845  climxlim2lem  45860  fperdvper  45934  stoweidlem35  46050  stoweidlem43  46058  stoweidlem59  46074  fourierdlem76  46197  etransclem47  46296  nnfoctbdjlem  46470  elprneb  47041  ichexmpl1  47456  ichnreuop  47459  vopnbgrel  47840  dfclnbgr6  47842  dfnbgr6  47843  usgrgrtrirex  47917  isubgr3stgrlem4  47936  usgrexmpl2trifr  47996  gpg3kgrtriex  48045  itcoval2  48585  itcoval3  48586  itcovalsuc  48588  ackvalsuc1mpt  48599  inlinecirc02plem  48707  oppcthinendcALT  49090