Theorem neeq1 3078

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ne 3017

This theorem is referenced by:  pm13.18  3097  nelrdva  3696  psseq1  4064  n0snor2el  4758  0inp0  5252  nnullss  5347  opeqex  5381  fri  5512  frsn  5634  xp11  6027  limeq  6198  tz6.12i  6691  fveqressseq  6842  funopsn  6905  fprg  6912  tpres  6958  f1dom3el3dif  7021  f1prex  7034  isofrlem  7087  f1oweALT  7667  frxp  7814  suppimacnv  7835  elqsn0  8360  frfi  8757  fiint  8789  marypha1lem  8891  eldju2ndl  9347  dfac8alem  9449  dfac8clem  9452  aceq3lem  9540  dfac5lem3  9545  dfac5lem4  9546  dfac5  9548  dfac2b  9550  dfac9  9556  kmlem1  9570  kmlem12  9581  kmlem14  9583  fin2i  9711  isfin2-2  9735  fin23lem21  9755  fin1a2lem10  9825  axcc2lem  9852  dominf  9861  ac5b  9894  zornn0g  9921  axdclem  9935  dominfac  9989  elwina  10102  elina  10103  iswun  10120  rankcf  10193  axrrecex  10579  elimne0  10625  1re  10635  recex  11266  xnn0nemnf  11972  uzn0  12254  qreccl  12362  xrnemnf  12506  xrnepnf  12507  xnn0n0n1ge2b  12520  fztpval  12963  expcl2lem  13435  hashnemnf  13698  hashneq0  13719  hashge2el2difr  13833  hashdmpropge2  13835  relexp1g  14379  ntrivcvgn0  15248  ntrivcvgmullem  15251  fprodntriv  15290  divalglem7  15744  divalg  15748  gcdcllem1  15842  gcdcllem3  15844  pcpre1  16173  pcqmul  16184  pcqcl  16187  prmgaplem3  16383  prmgaplem4  16384  xpsfrnel  16829  mreintcl  16860  isdrs  17538  isipodrs  17765  sgrp2rid2ex  18086  frgpuptinv  18891  isdrngrd  19522  isnzr2  20030  psgnodpmr  20728  lindfrn  20959  dmatelnd  21099  dmatmul  21100  mdetdiaglem  21201  mdetunilem1  21215  fvmptnn04ifa  21452  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  fiinopn  21503  hausnei  21930  dfconn2  22021  2ndcdisj  22058  regr1lem2  22342  isfbas  22431  ioorinv  24171  ioorcl  24172  vitalilem2  24204  vitalilem3  24205  vitali  24208  itg1climres  24309  mbfi1fseqlem4  24313  dvferm1lem  24575  dvferm2lem  24577  isuc1p  24728  ismon1p  24730  ply1remlem  24750  plydivlem4  24879  aannenlem1  24911  aannenlem2  24912  lgsne0  25905  lgsqr  25921  axtg5seg  26245  axtgupdim2  26251  axtgeucl  26252  axlowdim1  26739  lpvtx  26847  umgrnloopv  26885  usgrnloopvALT  26977  umgrvad2edg  26989  cusgrfilem2  27232  pthdlem2lem  27542  iswwlks  27608  iswwlksnx  27612  2pthdlem1  27703  isclwwlk  27756  3pthdlem1  27937  upgr3v3e3cycl  27953  upgr4cycl4dv4e  27958  eupth2lem2  27992  eupth2lem3lem4  28004  eupth2lem3lem6  28006  3cyclfrgrrn1  28058  4cycl2vnunb  28063  frgrreg  28167  norm1exi  29021  shintcl  29101  chintcl  29103  chne0  29265  elspansn2  29338  eigre  29606  eigorth  29609  kbpj  29727  superpos  30125  hatomic  30131  isprmidl  30950  ismxidl  30966  ssmxidllem  30973  ssmxidl  30974  xrge0iifhom  31175  xrge0iif1  31176  esumpr2  31321  sibfof  31593  signswn0  31825  signswch  31826  signstfvneq0  31837  axtgupdim2ALTV  31934  bnj168  31995  bnj970  32214  bnj1154  32266  umgracycusgr  32396  cusgracyclt3v  32398  subfacp1lem1  32421  erdszelem8  32440  indispconn  32476  cvmsss2  32516  nepss  32943  frmin  33079  elwlim  33105  nolesgn2ores  33174  nosepdmlem  33182  nosupbnd1lem3  33205  nosupbnd1lem5  33207  nosupbnd2lem1  33210  dfrdg4  33407  fvray  33597  linedegen  33599  fvline  33600  hilbert1.1  33610  rankeq1o  33627  unblimceq0lem  33840  knoppndvlem21  33866  poimirlem1  34887  poimirlem17  34903  poimirlem20  34906  poimirlem32  34918  itg2addnclem3  34939  neificl  35022  isdrngo3  35231  ispridl  35306  ismaxidl  35312  islshp  36109  lsatn0  36129  lshpset2N  36249  atlex  36446  hlsuprexch  36511  3dimlem1  36588  llni2  36642  lplni2  36667  2llnjN  36697  lvoli2  36711  2lplnj  36750  islinei  36870  lnatexN  36909  llnexchb2  36999  lhpmatb  37161  cdleme40m  37597  cdlemftr3  37695  cdlemk28-3  38038  cdlemk35s  38067  cdlemk39s  38069  cdlemk42  38071  nnn1suc  39152  dnnumch1  39637  aomclem3  39649  aomclem8  39654  dfac11  39655  dfacbasgrp  39701  dfsucon  39882  ax6e2ndeq  40886  ax6e2ndeqVD  41236  fnchoice  41279  fiiuncl  41320  disjrnmpt2  41441  idlimc  41899  limcperiod  41901  limclner  41924  cnrefiisp  42103  climxlim2lem  42118  fperdvper  42195  stoweidlem35  42313  stoweidlem43  42321  stoweidlem59  42337  fourierdlem76  42460  etransclem47  42559  nnfoctbdjlem  42730  elprneb  43257  ichexmpl1  43624  ichnreuop  43627  nrhmzr  44137  inlinecirc02plem  44766