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

Theorem neeq1 2609
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 2442 . . 3  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
21notbid 286 . 2  |-  ( A  =  B  ->  ( -.  A  =  C  <->  -.  B  =  C ) )
3 df-ne 2601 . 2  |-  ( A  =/=  C  <->  -.  A  =  C )
4 df-ne 2601 . 2  |-  ( B  =/=  C  <->  -.  B  =  C )
52, 3, 43bitr4g 280 1  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    = wceq 1652    =/= wne 2599
This theorem is referenced by:  neeq1i  2611  neeq1d  2614  nelrdva  3143  psseq1  3434  0inp0  4371  nnullss  4425  opeqex  4447  fri  4544  limeq  4593  xp11  5304  tz6.12i  5751  fprg  5915  isofrlem  6060  f1oweALT  6074  frxp  6456  elqsn0  6973  frfi  7352  fiint  7383  marypha1lem  7438  dfac8alem  7910  dfac8clem  7913  aceq3lem  8001  dfac5lem3  8006  dfac5lem4  8007  dfac5  8009  dfac2  8011  dfac9  8016  kmlem1  8030  kmlem12  8041  kmlem14  8043  fin2i  8175  isfin2-2  8199  fin23lem21  8219  fin1a2lem10  8289  axcc2lem  8316  dominf  8325  ac5b  8358  zornn0g  8385  axdclem  8399  dominfac  8448  elwina  8561  elina  8562  iswun  8579  rankcf  8652  axrrecex  9038  elimne0  9082  1re  9090  recex  9654  uzn0  10501  qreccl  10594  xrnemnf  10718  xrnepnf  10719  fztpval  11107  expcl2lem  11393  hashnemnf  11628  divalglem7  12919  divalg  12923  gcdcllem1  13011  gcdcllem3  13013  isprm2lem  13086  pcpre1  13216  pcqmul  13227  pcqcl  13230  xpscfv  13787  xpsfrnel  13788  mreintcl  13820  isdrs  14391  isipodrs  14587  frgpuptinv  15403  isdrngrd  15861  isnzr2  16334  fiinopn  16974  hausnei  17392  dfcon2  17482  2ndcdisj  17519  regr1lem2  17772  isfbas  17861  ioorinv  19468  ioorcl  19469  vitalilem2  19501  vitalilem3  19502  vitali  19505  itg1climres  19606  mbfi1fseqlem4  19610  dvferm1lem  19868  dvferm2lem  19870  isuc1p  20063  ismon1p  20065  ply1remlem  20085  plydivlem4  20213  aannenlem1  20245  aannenlem2  20246  lgsne0  21117  lgsqr  21130  usgranloopv  21398  usgra1v  21409  cusgrafilem2  21489  2pthoncl  21603  eupath2lem2  21700  eupath2lem3  21701  norm1exi  22752  shintcl  22832  chintcl  22834  chne0  22996  elspansn2  23069  eigre  23338  eigorth  23341  kbpj  23459  superpos  23857  hatomic  23863  xrge0iifhom  24323  xrge0iif1  24324  esumpr2  24458  sibfof  24654  subfacp1lem1  24865  erdszelem8  24884  indispcon  24921  cvmsss2  24961  nepss  25175  ntrivcvgn0  25226  ntrivcvgmullem  25229  fprodntriv  25268  frmin  25517  elwlim  25574  dfrdg4  25795  axlowdim1  25898  fvray  26075  linedegen  26077  fvline  26078  hilbert1.1  26088  rankeq1o  26112  itg2addnclem3  26258  neificl  26459  isdrngo3  26575  ispridl  26644  ismaxidl  26650  dnnumch1  27119  aomclem3  27131  aomclem8  27136  dfac11  27137  dfacbasgrp  27250  lindfrn  27268  fnchoice  27676  stoweidlem35  27760  stoweidlem43  27768  stoweidlem59  27784  3cyclfrgrarn1  28402  4cycl2vnunb  28407  frgrawopreglem3  28435  a9e2ndeq  28646  a9e2ndeqVD  29021  bnj168  29097  bnj970  29318  bnj1154  29368  islshp  29777  lsatn0  29797  lshpset2N  29917  atlex  30114  hlsuprexch  30178  3dimlem1  30255  llni2  30309  lplni2  30334  2llnjN  30364  lvoli2  30378  2lplnj  30417  islinei  30537  lnatexN  30576  llnexchb2  30666  lhpmatb  30828  cdleme40m  31264  cdlemftr3  31362  cdlemk28-3  31705  cdlemk35s  31734  cdlemk39s  31736  cdlemk42  31738
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 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429  df-ne 2601
  Copyright terms: Public domain W3C validator