Theorem neeq1 2575

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

Step	Hyp	Ref	Expression
1		eqeq1 2410	. . 3 |- ( A = B -> ( A = C <-> B = C ) )
2	1	notbid 286	. 2 |- ( A = B -> ( -. A = C <-> -. B = C ) )
3		df-ne 2569	. 2 |- ( A =/= C <-> -. A = C )
4		df-ne 2569	. 2 |- ( B =/= C <-> -. B = C )
5	2, 3, 4	3bitr4g 280	1 |- ( A = B -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   = wceq 1649   =/= wne 2567

This theorem is referenced by:  neeq1i  2577  neeq1d  2580  nelrdva  3103  psseq1  3394  0inp0  4331  nnullss  4385  opeqex  4407  fri  4504  limeq  4553  xp11  5263  tz6.12i  5710  fprg  5874  isofrlem  6019  f1oweALT  6033  frxp  6415  elqsn0  6932  frfi  7311  fiint  7342  marypha1lem  7396  dfac8alem  7866  dfac8clem  7869  aceq3lem  7957  dfac5lem3  7962  dfac5lem4  7963  dfac5  7965  dfac2  7967  dfac9  7972  kmlem1  7986  kmlem12  7997  kmlem14  7999  fin2i  8131  isfin2-2  8155  fin23lem21  8175  fin1a2lem10  8245  axcc2lem  8272  dominf  8281  ac5b  8314  zornn0g  8341  axdclem  8355  dominfac  8404  elwina  8517  elina  8518  iswun  8535  rankcf  8608  axrrecex  8994  elimne0  9038  1re  9046  recex  9610  uzn0  10457  qreccl  10550  xrnemnf  10674  xrnepnf  10675  fztpval  11063  expcl2lem  11348  hashnemnf  11583  divalglem7  12874  divalg  12878  gcdcllem1  12966  gcdcllem3  12968  isprm2lem  13041  pcpre1  13171  pcqmul  13182  pcqcl  13185  xpscfv  13742  xpsfrnel  13743  mreintcl  13775  isdrs  14346  isipodrs  14542  frgpuptinv  15358  isdrngrd  15816  isnzr2  16289  fiinopn  16929  hausnei  17346  dfcon2  17435  2ndcdisj  17472  regr1lem2  17725  isfbas  17814  ioorinv  19421  ioorcl  19422  vitalilem2  19454  vitalilem3  19455  vitali  19458  itg1climres  19559  mbfi1fseqlem4  19563  dvferm1lem  19821  dvferm2lem  19823  isuc1p  20016  ismon1p  20018  ply1remlem  20038  plydivlem4  20166  aannenlem1  20198  aannenlem2  20199  lgsne0  21070  lgsqr  21083  usgranloopv  21351  usgra1v  21362  cusgrafilem2  21442  2pthoncl  21556  eupath2lem2  21653  eupath2lem3  21654  norm1exi  22705  shintcl  22785  chintcl  22787  chne0  22949  elspansn2  23022  eigre  23291  eigorth  23294  kbpj  23412  superpos  23810  hatomic  23816  xrge0iifhom  24276  xrge0iif1  24277  esumpr2  24411  sibfof  24607  subfacp1lem1  24818  erdszelem8  24837  indispcon  24874  cvmsss2  24914  nepss  25128  ntrivcvgn0  25179  ntrivcvgmullem  25182  fprodntriv  25221  frmin  25456  dfrdg4  25703  axlowdim1  25802  fvray  25979  linedegen  25981  fvline  25982  hilbert1.1  25992  rankeq1o  26016  itg2addnclem3  26157  neificl  26349  isdrngo3  26465  ispridl  26534  ismaxidl  26540  dnnumch1  27009  aomclem3  27021  aomclem8  27027  dfac11  27028  dfacbasgrp  27141  lindfrn  27159  fnchoice  27567  stoweidlem35  27651  stoweidlem43  27659  stoweidlem59  27675  3cyclfrgrarn1  28116  4cycl2vnunb  28121  frgrawopreglem3  28149  a9e2ndeq  28357  a9e2ndeqVD  28730  bnj168  28803  bnj970  29024  bnj1154  29074  islshp  29462  lsatn0  29482  lshpset2N  29602  atlex  29799  hlsuprexch  29863  3dimlem1  29940  llni2  29994  lplni2  30019  2llnjN  30049  lvoli2  30063  2lplnj  30102  islinei  30222  lnatexN  30261  llnexchb2  30351  lhpmatb  30513  cdleme40m  30949  cdlemftr3  31047  cdlemk28-3  31390  cdlemk35s  31419  cdlemk39s  31421  cdlemk42  31423

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397  df-ne 2569