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

Theorem neeq2 2561
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 2398 . . 3  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
21notbid 286 . 2  |-  ( A  =  B  ->  ( -.  C  =  A  <->  -.  C  =  B ) )
3 df-ne 2554 . 2  |-  ( C  =/=  A  <->  -.  C  =  A )
4 df-ne 2554 . 2  |-  ( C  =/=  B  <->  -.  C  =  B )
52, 3, 43bitr4g 280 1  |-  ( A  =  B  ->  ( C  =/=  A  <->  C  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    = wceq 1649    =/= wne 2552
This theorem is referenced by:  neeq2i  2563  neeq2d  2566  psseq2  3380  fprg  5856  dfac5  7944  kmlem4  7968  kmlem14  7978  1re  9025  dvdsle  12824  isirred  15733  isnzr2  16263  hausnei  17316  regr1lem2  17695  xrhmeo  18844  2pthoncl  21453  superpos  23707  dfrdg4  25515  axlowdim1  25614  fvray  25791  linedegen  25793  fvline  25794  linethru  25803  hilbert1.1  25804  refsum2cnlem1  27378  stoweidlem43  27462  3cyclfrgrarn1  27767  4cycl2vnunb  27772  a9e2ndeq  27991  a9e2ndeqVD  28364  a9e2ndeqALT  28387  hlsuprexch  29497  3dim1lem5  29582  llni2  29628  lplni2  29653  2llnjN  29683  lvoli2  29697  2lplnj  29736  islinei  29856  cdleme40n  30584  cdlemg33b  30823
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2382  df-ne 2554
  Copyright terms: Public domain W3C validator