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

Theorem neeq2 2468
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
Assertion
Ref Expression
neeq2  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )

Proof of Theorem neeq2
StepHypRef Expression
1 eqeq2 2305 . . 3  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
21notbid 285 . 2  |-  ( A  =  B  ->  ( -.  C  =  A  <->  -.  C  =  B ) )
3 df-ne 2461 . 2  |-  ( C  =/=  A  <->  -.  C  =  A )
4 df-ne 2461 . 2  |-  ( C  =/=  B  <->  -.  C  =  B )
52, 3, 43bitr4g 279 1  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    = wceq 1632    =/= wne 2459
This theorem is referenced by:  neeq2i  2470  neeq2d  2473  psseq2  3277  dfac5  7771  kmlem4  7795  kmlem14  7805  1re  8853  dvdsle  12590  isirred  15497  isnzr2  16031  hausnei  17072  regr1lem2  17447  xrhmeo  18460  superpos  22950  dfrdg4  24560  axlowdim1  24659  fvray  24836  linedegen  24838  fvline  24839  linethru  24848  hilbert1.1  24849  fprg  25236  isig2a2  26169  isibg2aa  26215  isibg2aalem1  26216  isibg2aalem2  26217  refsum2cnlem1  27811  stoweidlem36  27888  stoweidlem43  27895  3cyclfrgrarn1  28435  4cycl2vnunb  28439  a9e2ndeq  28624  a9e2ndeqVD  29001  a9e2ndeqALT  29024  hlsuprexch  30192  3dim1lem5  30277  llni2  30323  lplni2  30348  2llnjN  30378  lvoli2  30392  2lplnj  30431  islinei  30551  cdleme40n  31279  cdlemg33b  31518
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator