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 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

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

This theorem is referenced by:  pm13.18  3023  pm13.181  3024  nelrdva  3702  psseq1  4088  n0snor2el  4835  0inp0  5358  nnullss  5463  opeqex  5499  friOLD  5638  frsn  5764  xp11  6175  limeq  6377  tz6.12i  6920  fveqressseq  7082  funopsn  7146  fprg  7153  tpres  7202  f1dom3el3dif  7268  f1prex  7282  isofrlem  7337  f1oweALT  7959  frxp  8112  xpord2lem  8128  poxp2  8129  frxp2  8130  xpord2indlem  8133  xpord3lem  8135  frxp3  8137  xpord3inddlem  8140  suppimacnv  8159  elqsn0  8780  frfi  9288  fiint  9324  marypha1lem  9428  frmin  9744  eldju2ndl  9919  dfac8alem  10024  dfac8clem  10027  aceq3lem  10115  dfac5lem3  10120  dfac5lem4  10121  dfac5  10123  dfac2b  10125  dfac9  10131  kmlem1  10145  kmlem12  10156  kmlem14  10158  fin2i  10290  isfin2-2  10314  fin23lem21  10334  fin1a2lem10  10404  axcc2lem  10431  dominf  10440  ac5b  10473  zornn0g  10500  axdclem  10514  dominfac  10568  elwina  10681  elina  10682  iswun  10699  rankcf  10772  axrrecex  11158  elimne0  11204  1re  11214  recex  11846  xnn0nemnf  12555  uzn0  12839  qreccl  12953  xrnemnf  13097  xrnepnf  13098  xnn0n0n1ge2b  13111  fztpval  13563  expcl2lem  14039  hashnemnf  14304  hashneq0  14324  hashge2el2difr  14442  hashdmpropge2  14444  relexp1g  14973  ntrivcvgn0  15844  ntrivcvgmullem  15847  fprodntriv  15886  divalglem7  16342  divalg  16346  gcdcllem1  16440  gcdcllem3  16442  pcpre1  16775  pcqmul  16786  pcqcl  16789  prmgaplem3  16986  prmgaplem4  16987  xpsfrnel  17508  mreintcl  17539  isdrs  18254  isipodrs  18490  sgrp2rid2ex  18808  frgpuptinv  19639  isnzr2  20297  isdrngrd  20391  isdrngrdOLD  20393  psgnodpmr  21143  lindfrn  21376  dmatelnd  21998  dmatmul  21999  mdetdiaglem  22100  mdetunilem1  22114  fvmptnn04ifa  22352  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  fiinopn  22403  hausnei  22832  dfconn2  22923  2ndcdisj  22960  regr1lem2  23244  isfbas  23333  ioorinv  25093  ioorcl  25094  vitalilem2  25126  vitalilem3  25127  vitali  25130  itg1climres  25232  mbfi1fseqlem4  25236  dvferm1lem  25501  dvferm2lem  25503  isuc1p  25658  ismon1p  25660  ply1remlem  25680  plydivlem4  25809  aannenlem1  25841  aannenlem2  25842  lgsne0  26838  lgsqr  26854  nolesgn2ores  27175  nogesgn1ores  27177  nosepdmlem  27186  nosupbnd1lem3  27213  nosupbnd1lem5  27215  nosupbnd2lem1  27218  noinfbnd1lem3  27228  noinfbnd1lem5  27230  noinfbnd2lem1  27233  axtg5seg  27716  axtgupdim2  27722  axtgeucl  27723  axlowdim1  28217  lpvtx  28328  umgrnloopv  28366  usgrnloopvALT  28458  umgrvad2edg  28470  cusgrfilem2  28713  pthdlem2lem  29024  iswwlks  29090  iswwlksnx  29094  2pthdlem1  29184  isclwwlk  29237  3pthdlem1  29417  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  eupth2lem2  29472  eupth2lem3lem4  29484  eupth2lem3lem6  29486  3cyclfrgrrn1  29538  4cycl2vnunb  29543  frgrreg  29647  norm1exi  30503  shintcl  30583  chintcl  30585  chne0  30747  elspansn2  30820  eigre  31088  eigorth  31091  kbpj  31209  superpos  31607  hatomic  31613  isprmidl  32556  ismxidl  32578  ssmxidllem  32589  ssmxidl  32590  zarcmplem  32861  xrge0iifhom  32917  xrge0iif1  32918  esumpr2  33065  sibfof  33339  signswn0  33571  signswch  33572  signstfvneq0  33583  axtgupdim2ALTV  33680  bnj168  33741  bnj970  33958  bnj1154  34010  umgracycusgr  34145  cusgracyclt3v  34147  subfacp1lem1  34170  erdszelem8  34189  indispconn  34225  cvmsss2  34265  nepss  34687  elwlim  34795  dfrdg4  34923  fvray  35113  linedegen  35115  fvline  35116  hilbert1.1  35126  rankeq1o  35143  unblimceq0lem  35382  knoppndvlem21  35408  poimirlem1  36489  poimirlem17  36505  poimirlem20  36508  poimirlem32  36520  itg2addnclem3  36541  neificl  36621  isdrngo3  36827  ispridl  36902  ismaxidl  36908  islshp  37849  lsatn0  37869  lshpset2N  37989  atlex  38186  hlsuprexch  38252  3dimlem1  38329  llni2  38383  lplni2  38408  2llnjN  38438  lvoli2  38452  2lplnj  38491  islinei  38611  lnatexN  38650  llnexchb2  38740  lhpmatb  38902  cdleme40m  39338  cdlemftr3  39436  cdlemk28-3  39779  cdlemk35s  39808  cdlemk39s  39810  cdlemk42  39812  metakunt30  41014  nnn1suc  41180  dnnumch1  41786  aomclem3  41798  aomclem8  41803  dfac11  41804  dfacbasgrp  41850  dfsucon  42274  ax6e2ndeq  43320  ax6e2ndeqVD  43670  fnchoice  43713  fiiuncl  43752  disjrnmpt2  43886  idlimc  44342  limcperiod  44344  limclner  44367  cnrefiisp  44546  climxlim2lem  44561  fperdvper  44635  stoweidlem35  44751  stoweidlem43  44759  stoweidlem59  44775  fourierdlem76  44898  etransclem47  44997  nnfoctbdjlem  45171  elprneb  45739  ichexmpl1  46137  ichnreuop  46140  nrhmzr  46647  itcoval2  47350  itcoval3  47351  itcovalsuc  47353  ackvalsuc1mpt  47364  inlinecirc02plem  47472