Theorem neeq1 3020

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	neeq1d 3017	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  pm13.18  3039  pm13.181  3040  nelrdva  3669  psseq1  4045  n0snor2el  4799  0inp0  5331  nnullss  5445  opeqex  5483  frsn  5751  xp11  6175  limeq  6374  tz6.12i  6909  fveqressseq  7076  funopsnOLD  7147  fprg  7154  tpres  7201  f1dom3el3dif  7269  f1ounsn  7272  f1prex  7284  isofrlem  7340  resf1extb  7932  f1oweALT  7970  frxp  8123  xpord2lem  8139  poxp2  8140  frxp2  8141  xpord2indlem  8144  xpord3lem  8146  frxp3  8148  xpord3inddlem  8151  suppimacnv  8171  elqsn0  8783  frfi  9246  fiint  9287  marypha1lem  9394  frmin  9722  eldju2ndl  9911  dfac8alem  10014  dfac8clem  10017  aceq3lem  10105  dfac5lem3  10110  dfac5lem4  10111  dfac5  10113  dfac2b  10115  dfac9  10121  kmlem1  10135  kmlem12  10146  kmlem14  10148  fin2i  10280  isfin2-2  10304  fin23lem21  10324  fin1a2lem10  10394  axcc2lem  10421  dominf  10430  ac5b  10463  zornn0g  10490  axdclem  10504  dominfac  10559  elwina  10672  elina  10673  iswun  10690  rankcf  10763  axrrecex  11149  elimne0  11197  1re  11209  recex  11847  xnn0nemnf  12589  uzn0  12880  qreccl  12994  xrnemnf  13143  xrnepnf  13144  xnn0n0n1ge2b  13158  fztpval  13616  expcl2lem  14111  hashnemnf  14382  hashneq0  14402  hashge2el2difr  14520  hashdmpropge2  14522  relexp1g  15065  ntrivcvgn0  15954  ntrivcvgmullem  15957  fprodntriv  15998  divalglem7  16458  divalg  16462  gcdcllem1  16558  gcdcllem3  16560  pcpre1  16903  pcqmul  16914  pcqcl  16917  prmgaplem3  17114  prmgaplem4  17115  xpsfrnel  17617  mreintcl  17648  isdrs  18358  isipodrs  18594  sgrp2rid2ex  18990  frgpuptinv  19842  isnzr2  20602  nrhmzr  20623  isdrngrd  20851  isdrngrdOLD  20853  isprmidl  21444  psgnodpmr  21721  lindfrn  21952  dmatelnd  22634  dmatmul  22635  mdetdiaglem  22736  mdetunilem1  22750  fvmptnn04ifa  22988  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  fiinopn  23039  hausnei  23466  dfconn2  23557  2ndcdisj  23594  regr1lem2  23878  isfbas  23967  ioorinv  25716  ioorcl  25717  vitalilem2  25749  vitalilem3  25750  vitali  25753  itg1climres  25854  mbfi1fseqlem4  25858  dvferm1lem  26124  dvferm2lem  26126  isuc1p  26279  ismon1p  26281  ply1remlem  26303  plydivlem4  26438  aannenlem1  26472  aannenlem2  26473  lgsne0  27480  lgsqr  27496  nolesgn2ores  27817  nogesgn1ores  27819  nosepdmlem  27828  nosupbnd1lem3  27855  nosupbnd1lem5  27857  nosupbnd2lem1  27860  noinfbnd1lem3  27870  noinfbnd1lem5  27872  noinfbnd2lem1  27875  axtg5seg  28715  axtgupdim2  28721  axtgeucl  28722  axlowdim1  29290  lpvtx  29399  umgrnloopv  29437  usgrnloopvALT  29532  umgrvad2edg  29544  cusgrfilem2  29787  pthdlem2lem  30097  iswwlks  30166  iswwlksnx  30170  2pthdlem1  30260  isclwwlk  30316  3pthdlem1  30496  upgr3v3e3cycl  30512  upgr4cycl4dv4e  30517  eupth2lem2  30551  eupth2lem3lem4  30563  eupth2lem3lem6  30565  3cyclfrgrrn1  30617  4cycl2vnunb  30622  frgrreg  30726  norm1exi  31583  shintcl  31663  chintcl  31665  chne0  31827  elspansn2  31900  eigre  32168  eigorth  32171  kbpj  32289  superpos  32687  hatomic  32693  ismxidl  33726  ssmxidllem  33737  ssmxidl  33738  constrconj  34116  constrcccllem  34125  constrcbvlem  34126  2sqr3minply  34151  zarcmplem  34252  xrge0iifhom  34308  xrge0iif1  34309  esumpr2  34438  sibfof  34711  signswn0  34928  signswch  34929  signstfvneq0  34940  axtgupdim2ALTV  35036  bnj168  35100  bnj970  35316  bnj1154  35368  onvf1odlem2  35569  umgracycusgr  35627  cusgracyclt3v  35629  subfacp1lem1  35652  erdszelem8  35671  indispconn  35707  cvmsss2  35747  nepss  36191  elwlim  36294  dfrdg4  36424  fvray  36614  linedegen  36616  fvline  36617  hilbert1.1  36627  rankeq1o  36644  unblimceq0lem  37076  knoppndvlem21  37102  qdiff  37952  poimirlem1  38253  poimirlem17  38269  poimirlem20  38272  poimirlem32  38284  itg2addnclem3  38305  neificl  38385  isdrngo3  38591  ispridl  38666  ismaxidl  38672  islshp  39734  lsatn0  39754  lshpset2N  39874  atlex  40071  hlsuprexch  40136  3dimlem1  40213  llni2  40267  lplni2  40292  2llnjN  40322  lvoli2  40336  2lplnj  40375  islinei  40495  lnatexN  40534  llnexchb2  40624  lhpmatb  40786  cdleme40m  41222  cdlemftr3  41320  cdlemk28-3  41663  cdlemk35s  41692  cdlemk39s  41694  cdlemk42  41696  nnn1suc  43014  dnnumch1  43754  aomclem3  43766  aomclem8  43771  dfac11  43772  dfacbasgrp  43818  dfsucon  44232  ax6e2ndeq  45251  ax6e2ndeqVD  45600  relpfrlem  45645  permac8prim  45706  fnchoice  45732  fiiuncl  45768  disjrnmpt2  45889  idlimc  46325  limcperiod  46327  limclner  46348  cnrefiisp  46527  climxlim2lem  46542  fperdvper  46616  stoweidlem35  46732  stoweidlem43  46740  stoweidlem59  46756  fourierdlem76  46879  etransclem47  46978  nnfoctbdjlem  47152  elprneb  47749  ichexmpl1  48201  ichnreuop  48204  vopnbgrel  48602  dfclnbgr6  48604  dfnbgr6  48605  usgrgrtrirex  48698  isubgr3stgrlem4  48717  usgrexmpl2trifr  48785  gpg3kgrtriex  48837  itcoval2  49427  itcoval3  49428  itcovalsuc  49430  ackvalsuc1mpt  49441  inlinecirc02plem  49549  oppcthinendcALT  50202