Theorem neeq1 3004

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2941

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-ne 2942

This theorem is referenced by:  pm13.18  3023  pm13.181  3024  nelrdva  3645  psseq1  4028  n0snor2el  4770  0inp0  5290  nnullss  5390  opeqex  5425  friOLD  5561  frsn  5685  xp11  6093  limeq  6293  tz6.12i  6832  fveqressseq  6989  funopsn  7052  fprg  7059  tpres  7108  f1dom3el3dif  7174  f1prex  7188  isofrlem  7243  f1oweALT  7847  frxp  7998  suppimacnv  8021  elqsn0  8606  frfi  9103  fiint  9135  marypha1lem  9236  frmin  9551  eldju2ndl  9726  dfac8alem  9831  dfac8clem  9834  aceq3lem  9922  dfac5lem3  9927  dfac5lem4  9928  dfac5  9930  dfac2b  9932  dfac9  9938  kmlem1  9952  kmlem12  9963  kmlem14  9965  fin2i  10097  isfin2-2  10121  fin23lem21  10141  fin1a2lem10  10211  axcc2lem  10238  dominf  10247  ac5b  10280  zornn0g  10307  axdclem  10321  dominfac  10375  elwina  10488  elina  10489  iswun  10506  rankcf  10579  axrrecex  10965  elimne0  11011  1re  11021  recex  11653  xnn0nemnf  12362  uzn0  12645  qreccl  12755  xrnemnf  12899  xrnepnf  12900  xnn0n0n1ge2b  12913  fztpval  13364  expcl2lem  13840  hashnemnf  14104  hashneq0  14124  hashge2el2difr  14240  hashdmpropge2  14242  relexp1g  14782  ntrivcvgn0  15655  ntrivcvgmullem  15658  fprodntriv  15697  divalglem7  16153  divalg  16157  gcdcllem1  16251  gcdcllem3  16253  pcpre1  16588  pcqmul  16599  pcqcl  16602  prmgaplem3  16799  prmgaplem4  16800  xpsfrnel  17318  mreintcl  17349  isdrs  18064  isipodrs  18300  sgrp2rid2ex  18611  frgpuptinv  19422  isdrngrd  20062  isnzr2  20579  psgnodpmr  20840  lindfrn  21073  dmatelnd  21690  dmatmul  21691  mdetdiaglem  21792  mdetunilem1  21806  fvmptnn04ifa  22044  chfacfscmulgsum  22054  chfacfpmmulgsum  22058  fiinopn  22095  hausnei  22524  dfconn2  22615  2ndcdisj  22652  regr1lem2  22936  isfbas  23025  ioorinv  24785  ioorcl  24786  vitalilem2  24818  vitalilem3  24819  vitali  24822  itg1climres  24924  mbfi1fseqlem4  24928  dvferm1lem  25193  dvferm2lem  25195  isuc1p  25350  ismon1p  25352  ply1remlem  25372  plydivlem4  25501  aannenlem1  25533  aannenlem2  25534  lgsne0  26528  lgsqr  26544  axtg5seg  26871  axtgupdim2  26877  axtgeucl  26878  axlowdim1  27372  lpvtx  27483  umgrnloopv  27521  usgrnloopvALT  27613  umgrvad2edg  27625  cusgrfilem2  27868  pthdlem2lem  28180  iswwlks  28246  iswwlksnx  28250  2pthdlem1  28340  isclwwlk  28393  3pthdlem1  28573  upgr3v3e3cycl  28589  upgr4cycl4dv4e  28594  eupth2lem2  28628  eupth2lem3lem4  28640  eupth2lem3lem6  28642  3cyclfrgrrn1  28694  4cycl2vnunb  28699  frgrreg  28803  norm1exi  29657  shintcl  29737  chintcl  29739  chne0  29901  elspansn2  29974  eigre  30242  eigorth  30245  kbpj  30363  superpos  30761  hatomic  30767  isprmidl  31658  ismxidl  31679  ssmxidllem  31686  ssmxidl  31687  zarcmplem  31876  xrge0iifhom  31932  xrge0iif1  31933  esumpr2  32080  sibfof  32352  signswn0  32584  signswch  32585  signstfvneq0  32596  axtgupdim2ALTV  32693  bnj168  32754  bnj970  32972  bnj1154  33024  umgracycusgr  33161  cusgracyclt3v  33163  subfacp1lem1  33186  erdszelem8  33205  indispconn  33241  cvmsss2  33281  nepss  33707  xpord2lem  33834  poxp2  33835  frxp2  33836  xpord2ind  33839  xpord3lem  33840  frxp3  33842  xpord3ind  33845  elwlim  33862  nolesgn2ores  33920  nogesgn1ores  33922  nosepdmlem  33931  nosupbnd1lem3  33958  nosupbnd1lem5  33960  nosupbnd2lem1  33963  noinfbnd1lem3  33973  noinfbnd1lem5  33975  noinfbnd2lem1  33978  dfrdg4  34298  fvray  34488  linedegen  34490  fvline  34491  hilbert1.1  34501  rankeq1o  34518  unblimceq0lem  34731  knoppndvlem21  34757  poimirlem1  35822  poimirlem17  35838  poimirlem20  35841  poimirlem32  35853  itg2addnclem3  35874  neificl  35955  isdrngo3  36161  ispridl  36236  ismaxidl  36242  islshp  37035  lsatn0  37055  lshpset2N  37175  atlex  37372  hlsuprexch  37437  3dimlem1  37514  llni2  37568  lplni2  37593  2llnjN  37623  lvoli2  37637  2lplnj  37676  islinei  37796  lnatexN  37835  llnexchb2  37925  lhpmatb  38087  cdleme40m  38523  cdlemftr3  38621  cdlemk28-3  38964  cdlemk35s  38993  cdlemk39s  38995  cdlemk42  38997  metakunt30  40196  nnn1suc  40333  dnnumch1  40907  aomclem3  40919  aomclem8  40924  dfac11  40925  dfacbasgrp  40971  dfsucon  41168  ax6e2ndeq  42217  ax6e2ndeqVD  42567  fnchoice  42610  fiiuncl  42651  disjrnmpt2  42770  idlimc  43216  limcperiod  43218  limclner  43241  cnrefiisp  43420  climxlim2lem  43435  fperdvper  43509  stoweidlem35  43625  stoweidlem43  43633  stoweidlem59  43649  fourierdlem76  43772  etransclem47  43871  nnfoctbdjlem  44043  elprneb  44581  ichexmpl1  44979  ichnreuop  44982  nrhmzr  45489  itcoval2  46068  itcoval3  46069  itcovalsuc  46071  ackvalsuc1mpt  46082  inlinecirc02plem  46190