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

Theorem neeq2 2607
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 2444 . . 3  |-  ( A  =  B  ->  ( C  =  A  <->  C  =  B ) )
21notbid 286 . 2  |-  ( A  =  B  ->  ( -.  C  =  A  <->  -.  C  =  B ) )
3 df-ne 2600 . 2  |-  ( C  =/=  A  <->  -.  C  =  A )
4 df-ne 2600 . 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 1652    =/= wne 2598
This theorem is referenced by:  neeq2i  2609  neeq2d  2612  psseq2  3427  fprg  5907  dfac5  8001  kmlem4  8025  kmlem14  8035  1re  9082  dvdsle  12887  isirred  15796  isnzr2  16326  hausnei  17384  regr1lem2  17764  xrhmeo  18963  2pthoncl  21595  superpos  23849  dfrdg4  25787  axlowdim1  25890  fvray  26067  linedegen  26069  fvline  26070  linethru  26079  hilbert1.1  26080  refsum2cnlem1  27675  stoweidlem43  27759  3cyclfrgrarn1  28339  4cycl2vnunb  28344  a9e2ndeq  28583  a9e2ndeqVD  28958  a9e2ndeqALT  28980  hlsuprexch  30115  3dim1lem5  30200  llni2  30246  lplni2  30271  2llnjN  30301  lvoli2  30315  2lplnj  30354  islinei  30474  cdleme40n  31202  cdlemg33b  31441
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428  df-ne 2600
  Copyright terms: Public domain W3C validator