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

Theorem neeq2 2698
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
Assertion
Ref Expression
neeq2  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )

Proof of Theorem neeq2
StepHypRef Expression
1 id 22 . 2  |-  ( A  =  B  ->  A  =  B )
21neeq2d 2695 1  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1454    =/= wne 2632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-cleq 2454  df-ne 2634
This theorem is referenced by:  psseq2  3532  fprg  6096  f1dom3el3dif  6193  f1prex  6206  dfac5  8584  kmlem4  8608  kmlem14  8618  1re  9667  hashge2el2difr  12670  dvdsle  14398  sgrp2rid2ex  16709  isirred  17975  isnzr2  18535  dmatelnd  19569  mdetdiaglem  19671  mdetunilem1  19685  mdetunilem2  19686  maducoeval2  19713  hausnei  20392  regr1lem2  20803  xrhmeo  22022  axtg5seg  24561  axtgupdim2  24567  axtgeucl  24568  ishlg  24695  tglnpt2  24734  axlowdim1  25037  2pthoncl  25381  clwlknclwlkdifs  25736  3cyclfrgrarn1  25788  4cycl2vnunb  25793  numclwwlk2lem1  25878  numclwlk2lem2f  25879  superpos  28055  signswch  29498  axtgupdim2OLD  29533  dfrdg4  30766  fvray  30956  linedegen  30958  fvline  30959  linethru  30968  hilbert1.1  30969  poimirlem1  31985  hlsuprexch  32990  3dim1lem5  33075  llni2  33121  lplni2  33146  2llnjN  33176  lvoli2  33190  2lplnj  33229  islinei  33349  cdleme40n  34079  cdlemg33b  34318  ax6e2ndeq  36969  ax6e2ndeqVD  37345  ax6e2ndeqALT  37367  refsum2cnlem1  37397  stoweidlem43  37941  nnfoctbdjlem  38330  elprneb  38749  structgrssvtxlem  39170  2pthdlem1  39878  3pthdlem1  39904  upgr3v3e3cycl  39920  upgr4cycl4dv4e  39925  usgvad2edg  39995
  Copyright terms: Public domain W3C validator