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

Theorem neeq2 3079
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 3076 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  psseq2  4064  prproe  4830  fprg  6910  f1dom3el3dif  7018  f1prex  7031  dfac5  9543  kmlem4  9568  kmlem14  9578  1re  10630  hashge2el2difr  13829  hashdmpropge2  13831  dvdsle  15650  sgrp2rid2ex  18032  isirred  19380  isnzr2  19966  dmatelnd  21035  mdetdiaglem  21137  mdetunilem1  21151  mdetunilem2  21152  maducoeval2  21179  hausnei  21866  regr1lem2  22278  xrhmeo  23479  axtg5seg  26179  axtgupdim2  26185  axtgeucl  26186  ishlg  26316  tglnpt2  26355  axlowdim1  26673  umgrvad2edg  26923  2pthdlem1  27637  3pthdlem1  27871  upgr3v3e3cycl  27887  upgr4cycl4dv4e  27892  eupth2lem3lem4  27938  3cyclfrgrrn1  27992  4cycl2vnunb  27997  numclwwlkovh  28080  numclwwlkovq  28081  numclwwlk2lem1  28083  numclwlk2lem2f  28084  superpos  30059  signswch  31731  axtgupdim2ALTV  31839  dfrdg4  33310  fvray  33500  linedegen  33502  fvline  33503  linethru  33512  hilbert1.1  33513  knoppndvlem21  33769  poimirlem1  34775  hlsuprexch  36399  3dim1lem5  36484  llni2  36530  lplni2  36555  2llnjN  36585  lvoli2  36599  2lplnj  36638  islinei  36758  cdleme40n  37486  cdlemg33b  37725  ax6e2ndeq  40773  ax6e2ndeqVD  41123  ax6e2ndeqALT  41145  refsum2cnlem1  41174  stoweidlem43  42209  nnfoctbdjlem  42618  elprneb  43145  ichnreuop  43481  inlinecirc02plem  44671
  Copyright terms: Public domain W3C validator