Theorem neeq1 2621

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 2449	. . 3 |- ( A = B -> ( A = C <-> B = C ) )
2	1	notbid 294	. 2 |- ( A = B -> ( -. A = C <-> -. B = C ) )
3		df-ne 2613	. 2 |- ( A =/= C <-> -. A = C )
4		df-ne 2613	. 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 1369   =/= wne 2611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436  df-ne 2613

This theorem is referenced by:  neeq1i  2623  neeq1d  2626  nelrdva  3173  psseq1  3448  0inp0  4469  nnullss  4559  opeqex  4587  fri  4687  limeq  4736  xp11  5278  tz6.12i  5715  fprg  5896  f1dom3el3dif  5986  isofrlem  6036  f1oweALT  6566  frxp  6687  suppimacnv  6706  elqsn0  7174  frfi  7562  fiint  7593  marypha1lem  7688  dfac8alem  8204  dfac8clem  8207  aceq3lem  8295  dfac5lem3  8300  dfac5lem4  8301  dfac5  8303  dfac2  8305  dfac9  8310  kmlem1  8324  kmlem12  8335  kmlem14  8337  fin2i  8469  isfin2-2  8493  fin23lem21  8513  fin1a2lem10  8583  axcc2lem  8610  dominf  8619  ac5b  8652  zornn0g  8679  axdclem  8693  dominfac  8742  elwina  8858  elina  8859  iswun  8876  rankcf  8949  axrrecex  9335  elimne0  9381  1re  9390  recex  9973  uzn0  10881  qreccl  10978  xrnemnf  11104  xrnepnf  11105  fztpval  11523  expcl2lem  11882  hashnemnf  12120  hashneq0  12137  divalglem7  13608  divalg  13612  gcdcllem1  13700  gcdcllem3  13702  isprm2lem  13775  pcpre1  13914  pcqmul  13925  pcqcl  13928  xpscfv  14505  xpsfrnel  14506  mreintcl  14538  isdrs  15109  isipodrs  15336  frgpuptinv  16273  isdrngrd  16863  isnzr2  17350  psgnodpmr  18025  lindfrn  18255  mdetunilem1  18423  fiinopn  18519  hausnei  18937  dfcon2  19028  2ndcdisj  19065  regr1lem2  19318  isfbas  19407  ioorinv  21061  ioorcl  21062  vitalilem2  21094  vitalilem3  21095  vitali  21098  itg1climres  21197  mbfi1fseqlem4  21201  dvferm1lem  21461  dvferm2lem  21463  isuc1p  21617  ismon1p  21619  ply1remlem  21639  plydivlem4  21767  aannenlem1  21799  aannenlem2  21800  lgsne0  22677  lgsqr  22690  axtg5seg  22931  axtgupdim2  22937  axtgeucl  22938  axlowdim1  23210  usgranloopv  23302  usgra1v  23313  cusgrafilem2  23393  2pthoncl  23507  eupath2lem2  23604  eupath2lem3  23605  norm1exi  24658  shintcl  24738  chintcl  24740  chne0  24902  elspansn2  24975  eigre  25244  eigorth  25247  kbpj  25365  superpos  25763  hatomic  25769  xrge0iifhom  26372  xrge0iif1  26373  esumpr2  26522  sibfof  26731  signswn0  26966  signswch  26967  signstfvneq0  26978  subfacp1lem1  27072  erdszelem8  27091  indispcon  27128  cvmsss2  27168  nepss  27379  ntrivcvgn0  27418  ntrivcvgmullem  27421  fprodntriv  27460  frmin  27708  elwlim  27765  dfrdg4  27986  fvray  28177  linedegen  28179  fvline  28180  hilbert1.1  28190  rankeq1o  28214  itg2addnclem3  28450  neificl  28654  isdrngo3  28770  ispridl  28839  ismaxidl  28845  dnnumch1  29402  aomclem3  29414  aomclem8  29419  dfac11  29420  dfacbasgrp  29469  fnchoice  29756  stoweidlem35  29835  stoweidlem43  29843  stoweidlem59  29859  wlkn0  30284  iswwlk  30322  3cyclfrgrarn1  30609  4cycl2vnunb  30614  frgrawopreglem3  30644  dmatelnd  30880  dmatmul  30881  dmatsubcl  30882  mdetdiaglem  30940  ax6e2ndeq  31273  ax6e2ndeqVD  31650  bnj168  31726  bnj970  31945  bnj1154  31995  islshp  32629  lsatn0  32649  lshpset2N  32769  atlex  32966  hlsuprexch  33030  3dimlem1  33107  llni2  33161  lplni2  33186  2llnjN  33216  lvoli2  33230  2lplnj  33269  islinei  33389  lnatexN  33428  llnexchb2  33518  lhpmatb  33680  cdleme40m  34116  cdlemftr3  34214  cdlemk28-3  34557  cdlemk35s  34586  cdlemk39s  34588  cdlemk42  34590