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

Theorem neeq1 2467
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 2302 . . 3  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
21notbid 285 . 2  |-  ( A  =  B  ->  ( -.  A  =  C  <->  -.  B  =  C ) )
3 df-ne 2461 . 2  |-  ( A  =/=  C  <->  -.  A  =  C )
4 df-ne 2461 . 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 1632    =/= wne 2459
This theorem is referenced by:  neeq1i  2469  neeq1d  2472  psseq1  3276  0inp0  4198  nnullss  4251  opeqex  4273  fri  4371  limeq  4420  xp11  5127  tz6.12i  5564  isofrlem  5853  f1oweALT  5867  frxp  6241  elqsn0  6744  frfi  7118  fiint  7149  marypha1lem  7202  dfac8alem  7672  dfac8clem  7675  aceq3lem  7763  dfac5lem3  7768  dfac5lem4  7769  dfac5  7771  dfac2  7773  dfac9  7778  kmlem1  7792  kmlem12  7803  kmlem14  7805  fin2i  7937  isfin2-2  7961  fin23lem21  7981  fin1a2lem10  8051  axcc2lem  8078  dominf  8087  ac5b  8121  zornn0g  8148  axdclem  8162  dominfac  8211  elwina  8324  elina  8325  iswun  8342  rankcf  8415  axrrecex  8801  elimne0  8845  1re  8853  recex  9416  uzn0  10259  qreccl  10352  xrnemnf  10476  xrnepnf  10477  fztpval  10861  expcl2lem  11131  divalglem7  12614  divalg  12618  gcdcllem1  12706  gcdcllem3  12708  isprm2lem  12781  pcpre1  12911  pcqmul  12922  pcqcl  12925  xpscfv  13480  xpsfrnel  13481  mreintcl  13513  isdrs  14084  isipodrs  14280  frgpuptinv  15096  isdrngrd  15554  isnzr2  16031  fiinopn  16663  hausnei  17072  dfcon2  17161  2ndcdisj  17198  regr1lem2  17447  isfbas  17540  ioorinv  18947  ioorcl  18948  vitalilem2  18980  vitalilem3  18981  vitali  18984  itg1climres  19085  mbfi1fseqlem4  19089  dvferm1lem  19347  dvferm2lem  19349  isuc1p  19542  ismon1p  19544  ply1remlem  19564  plydivlem4  19692  aannenlem1  19724  aannenlem2  19725  lgsne0  20588  lgsqr  20601  norm1exi  21845  shintcl  21925  chintcl  21927  chne0  22089  elspansn2  22162  eigre  22431  eigorth  22434  kbpj  22552  superpos  22950  hatomic  22956  disjex  23192  disjexc  23193  xrge0iifhom  23334  xrge0iif1  23335  esumpr2  23454  subfacp1lem1  23725  erdszelem8  23744  indispcon  23780  cvmsss2  23820  eupath2lem2  23917  eupath2lem3  23918  nepss  24087  zprodn0  24162  frmin  24313  dfrdg4  24560  axlowdim1  24659  fvray  24836  linedegen  24838  fvline  24839  hilbert1.1  24849  rankeq1o  24873  fprg  25236  osneisi  25634  islimrs4  25685  isig2a2  26169  isibg2aa  26215  isibg2aalem1  26216  nbssntrs  26250  neificl  26570  isdrngo3  26693  ispridl  26762  ismaxidl  26768  dnnumch1  27244  aomclem3  27256  aomclem8  27262  dfac11  27263  dfacbasgrp  27376  lindfrn  27394  fnchoice  27803  stoweidlem28  27880  stoweidlem35  27887  stoweidlem43  27895  stoweidlem59  27911  usgra1v  28260  3cyclfrgrarn1  28435  4cycl2vnunb  28439  a9e2ndeq  28624  a9e2ndeqVD  29001  bnj168  29074  bnj970  29295  bnj1154  29345  islshp  29791  lsatn0  29811  lshpset2N  29931  atlex  30128  hlsuprexch  30192  3dimlem1  30269  llni2  30323  lplni2  30348  2llnjN  30378  lvoli2  30392  2lplnj  30431  islinei  30551  lnatexN  30590  llnexchb2  30680  lhpmatb  30842  cdleme40m  31278  cdlemftr3  31376  cdlemk28-3  31719  cdlemk35s  31748  cdlemk39s  31750  cdlemk42  31752
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