Theorem neeq1 3007

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ≠ wne 2944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-ne 2945

This theorem is referenced by:  pm13.18  3026  pm13.181  3027  nelrdva  3643  psseq1  4026  n0snor2el  4769  0inp0  5284  nnullss  5379  opeqex  5414  friOLD  5549  frsn  5673  xp11  6075  limeq  6275  tz6.12i  6794  fveqressseq  6951  funopsn  7014  fprg  7021  tpres  7070  f1dom3el3dif  7136  f1prex  7149  isofrlem  7204  f1oweALT  7801  frxp  7951  suppimacnv  7974  elqsn0  8549  frfi  9020  fiint  9052  marypha1lem  9153  frmin  9490  frminOLD  9491  eldju2ndl  9666  dfac8alem  9769  dfac8clem  9772  aceq3lem  9860  dfac5lem3  9865  dfac5lem4  9866  dfac5  9868  dfac2b  9870  dfac9  9876  kmlem1  9890  kmlem12  9901  kmlem14  9903  fin2i  10035  isfin2-2  10059  fin23lem21  10079  fin1a2lem10  10149  axcc2lem  10176  dominf  10185  ac5b  10218  zornn0g  10245  axdclem  10259  dominfac  10313  elwina  10426  elina  10427  iswun  10444  rankcf  10517  axrrecex  10903  elimne0  10949  1re  10959  recex  11590  xnn0nemnf  12299  uzn0  12581  qreccl  12691  xrnemnf  12835  xrnepnf  12836  xnn0n0n1ge2b  12849  fztpval  13300  expcl2lem  13775  hashnemnf  14039  hashneq0  14060  hashge2el2difr  14176  hashdmpropge2  14178  relexp1g  14718  ntrivcvgn0  15591  ntrivcvgmullem  15594  fprodntriv  15633  divalglem7  16089  divalg  16093  gcdcllem1  16187  gcdcllem3  16189  pcpre1  16524  pcqmul  16535  pcqcl  16538  prmgaplem3  16735  prmgaplem4  16736  xpsfrnel  17254  mreintcl  17285  isdrs  18000  isipodrs  18236  sgrp2rid2ex  18547  frgpuptinv  19358  isdrngrd  19998  isnzr2  20515  psgnodpmr  20776  lindfrn  21009  dmatelnd  21626  dmatmul  21627  mdetdiaglem  21728  mdetunilem1  21742  fvmptnn04ifa  21980  chfacfscmulgsum  21990  chfacfpmmulgsum  21994  fiinopn  22031  hausnei  22460  dfconn2  22551  2ndcdisj  22588  regr1lem2  22872  isfbas  22961  ioorinv  24721  ioorcl  24722  vitalilem2  24754  vitalilem3  24755  vitali  24758  itg1climres  24860  mbfi1fseqlem4  24864  dvferm1lem  25129  dvferm2lem  25131  isuc1p  25286  ismon1p  25288  ply1remlem  25308  plydivlem4  25437  aannenlem1  25469  aannenlem2  25470  lgsne0  26464  lgsqr  26480  axtg5seg  26807  axtgupdim2  26813  axtgeucl  26814  axlowdim1  27308  lpvtx  27419  umgrnloopv  27457  usgrnloopvALT  27549  umgrvad2edg  27561  cusgrfilem2  27804  pthdlem2lem  28114  iswwlks  28180  iswwlksnx  28184  2pthdlem1  28274  isclwwlk  28327  3pthdlem1  28507  upgr3v3e3cycl  28523  upgr4cycl4dv4e  28528  eupth2lem2  28562  eupth2lem3lem4  28574  eupth2lem3lem6  28576  3cyclfrgrrn1  28628  4cycl2vnunb  28633  frgrreg  28737  norm1exi  29591  shintcl  29671  chintcl  29673  chne0  29835  elspansn2  29908  eigre  30176  eigorth  30179  kbpj  30297  superpos  30695  hatomic  30701  isprmidl  31592  ismxidl  31613  ssmxidllem  31620  ssmxidl  31621  zarcmplem  31810  xrge0iifhom  31866  xrge0iif1  31867  esumpr2  32014  sibfof  32286  signswn0  32518  signswch  32519  signstfvneq0  32530  axtgupdim2ALTV  32627  bnj168  32688  bnj970  32906  bnj1154  32958  umgracycusgr  33095  cusgracyclt3v  33097  subfacp1lem1  33120  erdszelem8  33139  indispconn  33175  cvmsss2  33215  nepss  33641  xpord2lem  33768  poxp2  33769  frxp2  33770  xpord2ind  33773  xpord3lem  33774  frxp3  33776  xpord3ind  33779  elwlim  33796  nolesgn2ores  33854  nogesgn1ores  33856  nosepdmlem  33865  nosupbnd1lem3  33892  nosupbnd1lem5  33894  nosupbnd2lem1  33897  noinfbnd1lem3  33907  noinfbnd1lem5  33909  noinfbnd2lem1  33912  dfrdg4  34232  fvray  34422  linedegen  34424  fvline  34425  hilbert1.1  34435  rankeq1o  34452  unblimceq0lem  34665  knoppndvlem21  34691  poimirlem1  35757  poimirlem17  35773  poimirlem20  35776  poimirlem32  35788  itg2addnclem3  35809  neificl  35890  isdrngo3  36096  ispridl  36171  ismaxidl  36177  islshp  36972  lsatn0  36992  lshpset2N  37112  atlex  37309  hlsuprexch  37374  3dimlem1  37451  llni2  37505  lplni2  37530  2llnjN  37560  lvoli2  37574  2lplnj  37613  islinei  37733  lnatexN  37772  llnexchb2  37862  lhpmatb  38024  cdleme40m  38460  cdlemftr3  38558  cdlemk28-3  38901  cdlemk35s  38930  cdlemk39s  38932  cdlemk42  38934  metakunt30  40134  nnn1suc  40276  dnnumch1  40849  aomclem3  40861  aomclem8  40866  dfac11  40867  dfacbasgrp  40913  dfsucon  41092  ax6e2ndeq  42132  ax6e2ndeqVD  42482  fnchoice  42525  fiiuncl  42566  disjrnmpt2  42679  idlimc  43121  limcperiod  43123  limclner  43146  cnrefiisp  43325  climxlim2lem  43340  fperdvper  43414  stoweidlem35  43530  stoweidlem43  43538  stoweidlem59  43554  fourierdlem76  43677  etransclem47  43776  nnfoctbdjlem  43947  elprneb  44474  ichexmpl1  44873  ichnreuop  44876  nrhmzr  45383  itcoval2  45962  itcoval3  45963  itcovalsuc  45965  ackvalsuc1mpt  45976  inlinecirc02plem  46084