Theorem neeq1 2614

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 2447	. . 3 |- ( A = B -> ( A = C <-> B = C ) )
2	1	notbid 294	. 2 |- ( A = B -> ( -. A = C <-> -. B = C ) )
3		df-ne 2606	. 2 |- ( A =/= C <-> -. A = C )
4		df-ne 2606	. 2 |- ( B =/= C <-> -. B = C )
5	2, 3, 4	3bitr4g 288	1 |- ( A = B -> ( A =/= C <-> B =/= C ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   = wceq 1364   =/= wne 2604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434  df-ne 2606

This theorem is referenced by:  neeq1i  2616  neeq1d  2619  nelrdva  3165  psseq1  3440  0inp0  4461  nnullss  4551  opeqex  4579  fri  4678  limeq  4727  xp11  5270  tz6.12i  5707  fprg  5888  f1dom3el3dif  5978  isofrlem  6028  f1oweALT  6560  frxp  6681  suppimacnv  6700  elqsn0  7165  frfi  7553  fiint  7584  marypha1lem  7679  dfac8alem  8195  dfac8clem  8198  aceq3lem  8286  dfac5lem3  8291  dfac5lem4  8292  dfac5  8294  dfac2  8296  dfac9  8301  kmlem1  8315  kmlem12  8326  kmlem14  8328  fin2i  8460  isfin2-2  8484  fin23lem21  8504  fin1a2lem10  8574  axcc2lem  8601  dominf  8610  ac5b  8643  zornn0g  8670  axdclem  8684  dominfac  8733  elwina  8849  elina  8850  iswun  8867  rankcf  8940  axrrecex  9326  elimne0  9372  1re  9381  recex  9964  uzn0  10872  qreccl  10969  xrnemnf  11095  xrnepnf  11096  fztpval  11514  expcl2lem  11873  hashnemnf  12111  hashneq0  12128  divalglem7  13599  divalg  13603  gcdcllem1  13691  gcdcllem3  13693  isprm2lem  13766  pcpre1  13905  pcqmul  13916  pcqcl  13919  xpscfv  14496  xpsfrnel  14497  mreintcl  14529  isdrs  15100  isipodrs  15327  frgpuptinv  16261  isdrngrd  16838  isnzr2  17323  psgnodpmr  17979  lindfrn  18209  mdetunilem1  18377  fiinopn  18473  hausnei  18891  dfcon2  18982  2ndcdisj  19019  regr1lem2  19272  isfbas  19361  ioorinv  21015  ioorcl  21016  vitalilem2  21048  vitalilem3  21049  vitali  21052  itg1climres  21151  mbfi1fseqlem4  21155  dvferm1lem  21415  dvferm2lem  21417  isuc1p  21571  ismon1p  21573  ply1remlem  21593  plydivlem4  21721  aannenlem1  21753  aannenlem2  21754  lgsne0  22631  lgsqr  22644  axtg5seg  22885  axtgupdim2  22891  axtgeucl  22892  axlowdim1  23140  usgranloopv  23232  usgra1v  23243  cusgrafilem2  23323  2pthoncl  23437  eupath2lem2  23534  eupath2lem3  23535  norm1exi  24588  shintcl  24668  chintcl  24670  chne0  24832  elspansn2  24905  eigre  25174  eigorth  25177  kbpj  25295  superpos  25693  hatomic  25699  xrge0iifhom  26303  xrge0iif1  26304  esumpr2  26453  sibfof  26656  signswn0  26891  signswch  26892  signstfvneq0  26903  subfacp1lem1  26997  erdszelem8  27016  indispcon  27053  cvmsss2  27093  nepss  27303  ntrivcvgn0  27342  ntrivcvgmullem  27345  fprodntriv  27384  frmin  27632  elwlim  27689  dfrdg4  27910  fvray  28101  linedegen  28103  fvline  28104  hilbert1.1  28114  rankeq1o  28138  itg2addnclem3  28370  neificl  28574  isdrngo3  28690  ispridl  28759  ismaxidl  28765  dnnumch1  29322  aomclem3  29334  aomclem8  29339  dfac11  29340  dfacbasgrp  29389  fnchoice  29676  stoweidlem35  29755  stoweidlem43  29763  stoweidlem59  29779  wlkn0  30204  iswwlk  30242  3cyclfrgrarn1  30529  4cycl2vnunb  30534  frgrawopreglem3  30564  dmatelnd  30758  dmatmul  30759  dmatsubcl  30760  mdetdiaglem  30776  ax6e2ndeq  31101  ax6e2ndeqVD  31479  bnj168  31555  bnj970  31774  bnj1154  31824  islshp  32346  lsatn0  32366  lshpset2N  32486  atlex  32683  hlsuprexch  32747  3dimlem1  32824  llni2  32878  lplni2  32903  2llnjN  32933  lvoli2  32947  2lplnj  32986  islinei  33106  lnatexN  33145  llnexchb2  33235  lhpmatb  33397  cdleme40m  33833  cdlemftr3  33931  cdlemk28-3  34274  cdlemk35s  34303  cdlemk39s  34305  cdlemk42  34307