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

Theorem neeq2 2844
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 2841 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wne 2779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-ne 2781
This theorem is referenced by:  psseq2  3656  fprg  6305  f1dom3el3dif  6404  f1prex  6417  dfac5  8812  kmlem4  8836  kmlem14  8846  1re  9896  hashge2el2difr  13071  dvdsle  14819  sgrp2rid2ex  17186  isirred  18471  isnzr2  19033  dmatelnd  20069  mdetdiaglem  20171  mdetunilem1  20185  mdetunilem2  20186  maducoeval2  20213  hausnei  20890  regr1lem2  21301  xrhmeo  22501  axtg5seg  25109  axtgupdim2  25115  axtgeucl  25116  ishlg  25243  tglnpt2  25282  axlowdim1  25585  2pthoncl  25927  clwlknclwlkdifs  26281  3cyclfrgrarn1  26333  4cycl2vnunb  26338  numclwwlk2lem1  26423  numclwlk2lem2f  26424  superpos  28431  signswch  29798  axtgupdim2OLD  29833  dfrdg4  31062  fvray  31252  linedegen  31254  fvline  31255  linethru  31264  hilbert1.1  31265  knoppndvlem21  31527  poimirlem1  32404  hlsuprexch  33509  3dim1lem5  33594  llni2  33640  lplni2  33665  2llnjN  33695  lvoli2  33709  2lplnj  33748  islinei  33868  cdleme40n  34598  cdlemg33b  34837  ax6e2ndeq  37620  ax6e2ndeqVD  37991  ax6e2ndeqALT  38013  refsum2cnlem1  38043  stoweidlem43  38760  nnfoctbdjlem  39172  elprneb  39764  structgrssvtxlem  40278  umgrvad2edg  40462  2pthdlem1  41159  clwwlknclwwlkdifs  41203  3pthdlem1  41353  upgr3v3e3cycl  41369  upgr4cycl4dv4e  41374  eupth2lem3lem4  41421  3cyclfrgrrn1  41477  4cycl2vnunb-av  41482  av-numclwwlkovq  41551  av-numclwwlk2lem1  41554  av-numclwlk2lem2f  41555
  Copyright terms: Public domain W3C validator