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

Theorem neeq2 3077
 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 3074 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ≠ wne 3014 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-ne 3015 This theorem is referenced by:  psseq2  4051  prproe  4823  fprg  6906  f1dom3el3dif  7017  f1prex  7030  dfac5  9548  kmlem4  9573  kmlem14  9583  1re  10635  hashge2el2difr  13842  hashdmpropge2  13844  dvdsle  15658  sgrp2rid2ex  18090  isirred  19447  isnzr2  20031  dmatelnd  21100  mdetdiaglem  21202  mdetunilem1  21216  mdetunilem2  21217  maducoeval2  21244  hausnei  21931  regr1lem2  22343  xrhmeo  23549  axtg5seg  26257  axtgupdim2  26263  axtgeucl  26264  ishlg  26394  tglnpt2  26433  axlowdim1  26751  umgrvad2edg  27001  2pthdlem1  27714  3pthdlem1  27947  upgr3v3e3cycl  27963  upgr4cycl4dv4e  27968  eupth2lem3lem4  28014  3cyclfrgrrn1  28068  4cycl2vnunb  28073  numclwwlkovh  28156  numclwwlkovq  28157  numclwwlk2lem1  28159  numclwlk2lem2f  28160  superpos  30135  signswch  31858  axtgupdim2ALTV  31966  dfrdg4  33439  fvray  33629  linedegen  33631  fvline  33632  linethru  33641  hilbert1.1  33642  knoppndvlem21  33898  poimirlem1  34970  hlsuprexch  36589  3dim1lem5  36674  llni2  36720  lplni2  36745  2llnjN  36775  lvoli2  36789  2lplnj  36828  islinei  36948  cdleme40n  37676  cdlemg33b  37915  ax6e2ndeq  41125  ax6e2ndeqVD  41475  ax6e2ndeqALT  41497  refsum2cnlem1  41526  stoweidlem43  42551  nnfoctbdjlem  42960  elprneb  43487  ichnreuop  43855  inlinecirc02plem  45054
 Copyright terms: Public domain W3C validator