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

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

Proof of Theorem neeq1
StepHypRef Expression
1 eqeq1 2289 . . 3  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
21notbid 285 . 2  |-  ( A  =  B  ->  ( -.  A  =  C  <->  -.  B  =  C ) )
3 df-ne 2448 . 2  |-  ( A  =/=  C  <->  -.  A  =  C )
4 df-ne 2448 . 2  |-  ( B  =/=  C  <->  -.  B  =  C )
52, 3, 43bitr4g 279 1  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    = wceq 1623    =/= wne 2446
This theorem is referenced by:  neeq1i  2456  neeq1d  2459  psseq1  3263  0inp0  4182  nnullss  4235  opeqex  4257  fri  4355  limeq  4404  xp11  5111  tz6.12i  5548  isofrlem  5837  f1oweALT  5851  frxp  6225  elqsn0  6728  frfi  7102  fiint  7133  marypha1lem  7186  dfac8alem  7656  dfac8clem  7659  aceq3lem  7747  dfac5lem3  7752  dfac5lem4  7753  dfac5  7755  dfac2  7757  dfac9  7762  kmlem1  7776  kmlem12  7787  kmlem14  7789  fin2i  7921  isfin2-2  7945  fin23lem21  7965  fin1a2lem10  8035  axcc2lem  8062  dominf  8071  ac5b  8105  zornn0g  8132  axdclem  8146  dominfac  8195  elwina  8308  elina  8309  iswun  8326  rankcf  8399  axrrecex  8785  elimne0  8829  1re  8837  recex  9400  uzn0  10243  qreccl  10336  xrnemnf  10460  xrnepnf  10461  fztpval  10845  expcl2lem  11115  divalglem7  12598  divalg  12602  gcdcllem1  12690  gcdcllem3  12692  isprm2lem  12765  pcpre1  12895  pcqmul  12906  pcqcl  12909  xpscfv  13464  xpsfrnel  13465  mreintcl  13497  isdrs  14068  isipodrs  14264  frgpuptinv  15080  isdrngrd  15538  isnzr2  16015  fiinopn  16647  hausnei  17056  dfcon2  17145  2ndcdisj  17182  regr1lem2  17431  isfbas  17524  ioorinv  18931  ioorcl  18932  vitalilem2  18964  vitalilem3  18965  vitali  18968  itg1climres  19069  mbfi1fseqlem4  19073  dvferm1lem  19331  dvferm2lem  19333  isuc1p  19526  ismon1p  19528  ply1remlem  19548  plydivlem4  19676  aannenlem1  19708  aannenlem2  19709  lgsne0  20572  lgsqr  20585  norm1exi  21829  shintcl  21909  chintcl  21911  chne0  22073  elspansn2  22146  eigre  22415  eigorth  22418  kbpj  22536  superpos  22934  hatomic  22940  disjex  23176  disjexc  23177  xrge0iifhom  23319  xrge0iif1  23320  esumpr2  23439  subfacp1lem1  23710  erdszelem8  23729  indispcon  23765  cvmsss2  23805  eupath2lem2  23902  eupath2lem3  23903  nepss  24072  frmin  24242  dfrdg4  24488  axlowdim1  24587  fvray  24764  linedegen  24766  fvline  24767  hilbert1.1  24777  rankeq1o  24801  fprg  25133  osneisi  25531  islimrs4  25582  isig2a2  26066  isibg2aa  26112  isibg2aalem1  26113  nbssntrs  26147  neificl  26467  isdrngo3  26590  ispridl  26659  ismaxidl  26665  dnnumch1  27141  aomclem3  27153  aomclem8  27159  dfac11  27160  dfacbasgrp  27273  lindfrn  27291  fnchoice  27700  stoweidlem28  27777  stoweidlem35  27784  stoweidlem43  27792  stoweidlem59  27808  usgra1v  28126  a9e2ndeq  28325  a9e2ndeqVD  28685  bnj168  28758  bnj970  28979  bnj1154  29029  islshp  29169  lsatn0  29189  lshpset2N  29309  atlex  29506  hlsuprexch  29570  3dimlem1  29647  llni2  29701  lplni2  29726  2llnjN  29756  lvoli2  29770  2lplnj  29809  islinei  29929  lnatexN  29968  llnexchb2  30058  lhpmatb  30220  cdleme40m  30656  cdlemftr3  30754  cdlemk28-3  31097  cdlemk35s  31126  cdlemk39s  31128  cdlemk42  31130
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