MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeq2 Structured version   Visualization version   GIF version

Theorem neeq2 2995
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
Assertion
Ref Expression
neeq2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))

Proof of Theorem neeq2
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21neeq2d 2992 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  wne 2932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-ne 2933
This theorem is referenced by:  psseq2  3837  prproe  4586  fprg  6585  f1dom3el3dif  6689  f1prex  6702  dfac5  9141  kmlem4  9167  kmlem14  9177  1re  10231  hashge2el2difr  13455  hashdmpropge2  13457  dvdsle  15234  sgrp2rid2ex  17615  isirred  18899  isnzr2  19465  dmatelnd  20504  mdetdiaglem  20606  mdetunilem1  20620  mdetunilem2  20621  maducoeval2  20648  hausnei  21334  regr1lem2  21745  xrhmeo  22946  axtg5seg  25563  axtgupdim2  25569  axtgeucl  25570  ishlg  25696  tglnpt2  25735  axlowdim1  26038  structgrssvtxlemOLD  26114  umgrvad2edg  26304  2pthdlem1  27050  clwwlknclwwlkdifsOLD  27102  3pthdlem1  27316  upgr3v3e3cycl  27332  upgr4cycl4dv4e  27337  eupth2lem3lem4  27383  3cyclfrgrrn1  27439  4cycl2vnunb  27444  numclwwlkovh  27534  numclwwlkovq  27535  numclwwlk2lem1  27537  numclwlk2lem2f  27538  numclwwlk2lem1OLD  27544  numclwlk2lem2fOLD  27545  superpos  29522  signswch  30947  axtgupdim2OLD  31055  dfrdg4  32364  fvray  32554  linedegen  32556  fvline  32557  linethru  32566  hilbert1.1  32567  knoppndvlem21  32829  poimirlem1  33723  hlsuprexch  35170  3dim1lem5  35255  llni2  35301  lplni2  35326  2llnjN  35356  lvoli2  35370  2lplnj  35409  islinei  35529  cdleme40n  36258  cdlemg33b  36497  ax6e2ndeq  39277  ax6e2ndeqVD  39644  ax6e2ndeqALT  39666  refsum2cnlem1  39695  stoweidlem43  40763  nnfoctbdjlem  41175  elprneb  41805
  Copyright terms: Public domain W3C validator