Theorem neeq1 2995

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 2992	1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2933

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 2709

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

This theorem is referenced by:  pm13.18  3014  pm13.181  3015  nelrdva  3665  psseq1  4044  n0snor2el  4791  0inp0  5306  nnullss  5417  opeqex  5454  frsn  5720  xp11  6141  limeq  6337  tz6.12i  6868  fveqressseq  7033  funopsn  7103  fprg  7110  tpres  7157  f1dom3el3dif  7225  f1ounsn  7228  f1prex  7240  isofrlem  7296  resf1extb  7886  f1oweALT  7926  frxp  8078  xpord2lem  8094  poxp2  8095  frxp2  8096  xpord2indlem  8099  xpord3lem  8101  frxp3  8103  xpord3inddlem  8106  suppimacnv  8126  elqsn0  8733  frfi  9197  fiint  9239  marypha1lem  9348  frmin  9673  eldju2ndl  9848  dfac8alem  9951  dfac8clem  9954  aceq3lem  10042  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  dfac5  10051  dfac2b  10053  dfac9  10059  kmlem1  10073  kmlem12  10084  kmlem14  10086  fin2i  10217  isfin2-2  10241  fin23lem21  10261  fin1a2lem10  10331  axcc2lem  10358  dominf  10367  ac5b  10400  zornn0g  10427  axdclem  10441  dominfac  10496  elwina  10609  elina  10610  iswun  10627  rankcf  10700  axrrecex  11086  elimne0  11134  1re  11144  recex  11781  xnn0nemnf  12497  uzn0  12780  qreccl  12894  xrnemnf  13043  xrnepnf  13044  xnn0n0n1ge2b  13058  fztpval  13514  expcl2lem  14008  hashnemnf  14279  hashneq0  14299  hashge2el2difr  14416  hashdmpropge2  14418  relexp1g  14961  ntrivcvgn0  15833  ntrivcvgmullem  15836  fprodntriv  15877  divalglem7  16338  divalg  16342  gcdcllem1  16438  gcdcllem3  16440  pcpre1  16782  pcqmul  16793  pcqcl  16796  prmgaplem3  16993  prmgaplem4  16994  xpsfrnel  17495  mreintcl  17526  isdrs  18236  isipodrs  18472  sgrp2rid2ex  18864  frgpuptinv  19712  isnzr2  20463  nrhmzr  20482  isdrngrd  20711  isdrngrdOLD  20713  psgnodpmr  21557  lindfrn  21788  dmatelnd  22452  dmatmul  22453  mdetdiaglem  22554  mdetunilem1  22568  fvmptnn04ifa  22806  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  fiinopn  22857  hausnei  23284  dfconn2  23375  2ndcdisj  23412  regr1lem2  23696  isfbas  23785  ioorinv  25545  ioorcl  25546  vitalilem2  25578  vitalilem3  25579  vitali  25582  itg1climres  25683  mbfi1fseqlem4  25687  dvferm1lem  25956  dvferm2lem  25958  isuc1p  26114  ismon1p  26116  ply1remlem  26138  plydivlem4  26272  aannenlem1  26304  aannenlem2  26305  lgsne0  27314  lgsqr  27330  nolesgn2ores  27652  nogesgn1ores  27654  nosepdmlem  27663  nosupbnd1lem3  27690  nosupbnd1lem5  27692  nosupbnd2lem1  27695  noinfbnd1lem3  27705  noinfbnd1lem5  27707  noinfbnd2lem1  27710  axtg5seg  28549  axtgupdim2  28555  axtgeucl  28556  axlowdim1  29044  lpvtx  29153  umgrnloopv  29191  usgrnloopvALT  29286  umgrvad2edg  29298  cusgrfilem2  29542  pthdlem2lem  29852  iswwlks  29921  iswwlksnx  29925  2pthdlem1  30015  isclwwlk  30071  3pthdlem1  30251  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  eupth2lem2  30306  eupth2lem3lem4  30318  eupth2lem3lem6  30320  3cyclfrgrrn1  30372  4cycl2vnunb  30377  frgrreg  30481  norm1exi  31337  shintcl  31417  chintcl  31419  chne0  31581  elspansn2  31654  eigre  31922  eigorth  31925  kbpj  32043  superpos  32441  hatomic  32447  isprmidl  33530  ismxidl  33554  ssmxidllem  33565  ssmxidl  33566  constrconj  33922  constrcccllem  33931  constrcbvlem  33932  2sqr3minply  33957  zarcmplem  34058  xrge0iifhom  34114  xrge0iif1  34115  esumpr2  34244  sibfof  34517  signswn0  34737  signswch  34738  signstfvneq0  34749  axtgupdim2ALTV  34845  bnj168  34906  bnj970  35122  bnj1154  35174  onvf1odlem2  35317  umgracycusgr  35367  cusgracyclt3v  35369  subfacp1lem1  35392  erdszelem8  35411  indispconn  35447  cvmsss2  35487  nepss  35931  elwlim  36034  dfrdg4  36164  fvray  36354  linedegen  36356  fvline  36357  hilbert1.1  36367  rankeq1o  36384  unblimceq0lem  36725  knoppndvlem21  36751  poimirlem1  37869  poimirlem17  37885  poimirlem20  37888  poimirlem32  37900  itg2addnclem3  37921  neificl  38001  isdrngo3  38207  ispridl  38282  ismaxidl  38288  islshp  39352  lsatn0  39372  lshpset2N  39492  atlex  39689  hlsuprexch  39754  3dimlem1  39831  llni2  39885  lplni2  39910  2llnjN  39940  lvoli2  39954  2lplnj  39993  islinei  40113  lnatexN  40152  llnexchb2  40242  lhpmatb  40404  cdleme40m  40840  cdlemftr3  40938  cdlemk28-3  41281  cdlemk35s  41310  cdlemk39s  41312  cdlemk42  41314  nnn1suc  42633  dnnumch1  43398  aomclem3  43410  aomclem8  43415  dfac11  43416  dfacbasgrp  43462  dfsucon  43876  ax6e2ndeq  44912  ax6e2ndeqVD  45261  relpfrlem  45306  permac8prim  45367  fnchoice  45386  fiiuncl  45422  disjrnmpt2  45544  idlimc  45983  limcperiod  45985  limclner  46006  cnrefiisp  46185  climxlim2lem  46200  fperdvper  46274  stoweidlem35  46390  stoweidlem43  46398  stoweidlem59  46414  fourierdlem76  46537  etransclem47  46636  nnfoctbdjlem  46810  elprneb  47386  ichexmpl1  47826  ichnreuop  47829  vopnbgrel  48211  dfclnbgr6  48213  dfnbgr6  48214  usgrgrtrirex  48307  isubgr3stgrlem4  48326  usgrexmpl2trifr  48394  gpg3kgrtriex  48446  itcoval2  49021  itcoval3  49022  itcovalsuc  49024  ackvalsuc1mpt  49035  inlinecirc02plem  49143  oppcthinendcALT  49797