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

Theorem neeq2 2886
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 2883 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  psseq2  3728  prproe  4466  fprg  6462  f1dom3el3dif  6566  f1prex  6579  dfac5  8989  kmlem4  9013  kmlem14  9023  1re  10077  hashge2el2difr  13301  hashdmpropge2  13303  dvdsle  15079  sgrp2rid2ex  17461  isirred  18745  isnzr2  19311  dmatelnd  20350  mdetdiaglem  20452  mdetunilem1  20466  mdetunilem2  20467  maducoeval2  20494  hausnei  21180  regr1lem2  21591  xrhmeo  22792  axtg5seg  25409  axtgupdim2  25415  axtgeucl  25416  ishlg  25542  tglnpt2  25581  axlowdim1  25884  structgrssvtxlemOLD  25960  umgrvad2edg  26150  2pthdlem1  26895  clwwlknclwwlkdifsOLD  26947  3pthdlem1  27142  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  eupth2lem3lem4  27209  3cyclfrgrrn1  27265  4cycl2vnunb  27270  numclwwlkovh  27353  numclwwlkovq  27354  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  superpos  29341  signswch  30766  axtgupdim2OLD  30874  dfrdg4  32183  fvray  32373  linedegen  32375  fvline  32376  linethru  32385  hilbert1.1  32386  knoppndvlem21  32648  poimirlem1  33540  hlsuprexch  34985  3dim1lem5  35070  llni2  35116  lplni2  35141  2llnjN  35171  lvoli2  35185  2lplnj  35224  islinei  35344  cdleme40n  36073  cdlemg33b  36312  ax6e2ndeq  39092  ax6e2ndeqVD  39459  ax6e2ndeqALT  39481  refsum2cnlem1  39510  stoweidlem43  40578  nnfoctbdjlem  40990  elprneb  41620
  Copyright terms: Public domain W3C validator