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

Theorem neeq2 2455
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 2292 . . 3  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
21notbid 285 . 2  |-  ( A  =  B  ->  ( -.  C  =  A  <->  -.  C  =  B ) )
3 df-ne 2448 . 2  |-  ( C  =/=  A  <->  -.  C  =  A )
4 df-ne 2448 . 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 1623    =/= wne 2446
This theorem is referenced by:  neeq2i  2457  neeq2d  2460  psseq2  3264  dfac5  7755  kmlem4  7779  kmlem14  7789  1re  8837  dvdsle  12574  isirred  15481  isnzr2  16015  hausnei  17056  regr1lem2  17431  xrhmeo  18444  superpos  22934  dfrdg4  23899  axlowdim1  23998  fvray  24175  linedegen  24177  fvline  24178  linethru  24187  hilbert1.1  24188  fprg  24545  isig2a2  25478  isibg2aa  25524  isibg2aalem1  25525  isibg2aalem2  25526  refsum2cnlem1  27120  stoweidlem36  27197  stoweidlem43  27204  a9e2ndeq  27698  a9e2ndeqVD  28058  a9e2ndeqALT  28081  hlsuprexch  28943  3dim1lem5  29028  llni2  29074  lplni2  29099  2llnjN  29129  lvoli2  29143  2lplnj  29182  islinei  29302  cdleme40n  30030  cdlemg33b  30269
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator