Theorem neeq1 3023

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ≠ wne 2961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-ne 2962

This theorem is referenced by:  pm13.18  3042  nelrdva  3604  psseq1  3948  n0snor2el  4634  0inp0  5109  nnullss  5207  opeqex  5240  fri  5365  frsn  5485  xp11  5869  limeq  6038  tz6.12i  6522  fveqressseq  6670  funopsn  6731  fprg  6738  tpres  6788  f1dom3el3dif  6850  f1prex  6863  isofrlem  6914  f1oweALT  7483  frxp  7623  suppimacnv  7642  elqsn0  8164  frfi  8556  fiint  8588  marypha1lem  8690  eldju2ndl  9145  dfac8alem  9247  dfac8clem  9250  aceq3lem  9338  dfac5lem3  9343  dfac5lem4  9344  dfac5  9346  dfac2b  9348  dfac9  9354  kmlem1  9368  kmlem12  9379  kmlem14  9381  fin2i  9513  isfin2-2  9537  fin23lem21  9557  fin1a2lem10  9627  axcc2lem  9654  dominf  9663  ac5b  9696  zornn0g  9723  axdclem  9737  dominfac  9791  elwina  9904  elina  9905  iswun  9922  rankcf  9995  axrrecex  10381  elimne0  10427  1re  10437  recex  11071  xnn0nemnf  11788  uzn0  12072  qreccl  12181  xrnemnf  12327  xrnepnf  12328  xnn0n0n1ge2b  12341  fztpval  12783  expcl2lem  13254  hashnemnf  13517  hashneq0  13538  hashge2el2difr  13648  hashdmpropge2  13650  relexp1g  14244  ntrivcvgn0  15112  ntrivcvgmullem  15115  fprodntriv  15154  divalglem7  15608  divalg  15612  gcdcllem1  15706  gcdcllem3  15708  pcpre1  16033  pcqmul  16044  pcqcl  16047  prmgaplem3  16243  prmgaplem4  16244  xpscfv  16691  xpsfrnel  16696  mreintcl  16736  isdrs  17414  isipodrs  17641  sgrp2rid2ex  17895  frgpuptinv  18669  isdrngrd  19263  isnzr2  19769  psgnodpmr  20448  lindfrn  20679  dmatelnd  20821  dmatmul  20822  mdetdiaglem  20923  mdetunilem1  20937  fvmptnn04ifa  21174  chfacfscmulgsum  21184  chfacfpmmulgsum  21188  fiinopn  21225  hausnei  21652  dfconn2  21743  2ndcdisj  21780  regr1lem2  22064  isfbas  22153  ioorinv  23892  ioorcl  23893  vitalilem2  23925  vitalilem3  23926  vitali  23929  itg1climres  24030  mbfi1fseqlem4  24034  dvferm1lem  24296  dvferm2lem  24298  isuc1p  24449  ismon1p  24451  ply1remlem  24471  plydivlem4  24600  aannenlem1  24632  aannenlem2  24633  lgsne0  25625  lgsqr  25641  axtg5seg  25965  axtgupdim2  25971  axtgeucl  25972  axlowdim1  26460  lpvtx  26568  umgrnloopv  26606  usgrnloopvALT  26698  umgrvad2edg  26710  cusgrfilem2  26953  pthdlem2lem  27268  iswwlks  27334  iswwlksnx  27338  2pthdlem1  27448  isclwwlk  27502  3pthdlem1  27705  upgr3v3e3cycl  27721  upgr4cycl4dv4e  27726  eupth2lem2  27761  eupth2lem3lem4  27773  eupth2lem3lem6  27775  3cyclfrgrrn1  27831  4cycl2vnunb  27836  frgrreg  27963  norm1exi  28818  shintcl  28900  chintcl  28902  chne0  29064  elspansn2  29137  eigre  29405  eigorth  29408  kbpj  29526  superpos  29924  hatomic  29930  xrge0iifhom  30853  xrge0iif1  30854  esumpr2  30999  sibfof  31272  signswn0  31505  signswch  31506  signstfvneq0  31518  axtgupdim2OLD  31616  bnj168  31677  bnj970  31895  bnj1154  31945  subfacp1lem1  32040  erdszelem8  32059  indispconn  32095  cvmsss2  32135  nepss  32497  frmin  32634  elwlim  32660  nolesgn2ores  32729  nosepdmlem  32737  nosupbnd1lem3  32760  nosupbnd1lem5  32762  nosupbnd2lem1  32765  dfrdg4  32962  fvray  33152  linedegen  33154  fvline  33155  hilbert1.1  33165  rankeq1o  33182  unblimceq0lem  33394  knoppndvlem21  33420  poimirlem1  34363  poimirlem17  34379  poimirlem20  34382  poimirlem32  34394  itg2addnclem3  34415  neificl  34499  isdrngo3  34708  ispridl  34783  ismaxidl  34789  islshp  35589  lsatn0  35609  lshpset2N  35729  atlex  35926  hlsuprexch  35991  3dimlem1  36068  llni2  36122  lplni2  36147  2llnjN  36177  lvoli2  36191  2lplnj  36230  islinei  36350  lnatexN  36389  llnexchb2  36479  lhpmatb  36641  cdleme40m  37077  cdlemftr3  37175  cdlemk28-3  37518  cdlemk35s  37547  cdlemk39s  37549  cdlemk42  37551  nnn1suc  38623  dnnumch1  39069  aomclem3  39081  aomclem8  39086  dfac11  39087  dfacbasgrp  39133  ax6e2ndeq  40341  ax6e2ndeqVD  40691  fnchoice  40734  fiiuncl  40775  disjrnmpt2  40899  idlimc  41363  limcperiod  41365  limclner  41388  cnrefiisp  41567  climxlim2lem  41582  fperdvper  41658  stoweidlem35  41776  stoweidlem43  41784  stoweidlem59  41800  fourierdlem76  41923  etransclem47  42022  nnfoctbdjlem  42193  elprneb  42694  ichexmpl1  43024  ichnreuop  43027  nrhmzr  43533  inlinecirc02plem  44166