Theorem neeq1 2024

Description: Equality theorem for inequality.

Assertion

Ref	Expression
neeq1	|- (A = B -> (A =/= C <-> B =/= C))

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		eqeq1 1890	. . 3 |- (A = B -> (A = C <-> B = C))
2	1	notbid 673	. 2 |- (A = B -> (-. A = C <-> -. B = C))
3		df-ne 2019	. 2 |- (A =/= C <-> -. A = C)
4		df-ne 2019	. 2 |- (B =/= C <-> -. B = C)
5	2, 3, 4	3bitr4g 614	1 |- (A = B -> (A =/= C <-> B =/= C))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   = wceq 1298   =/= wne 2017

This theorem is referenced by:  neeq1i 2026  neeq1d 2028  psseq1 2697  0inp0 3475  nnullss 3515  fri 3626  frc 3629  limeq 3669  limeqOLD 3670  xp11 4347  tz6.12i 4698  isofrlem 4878  f1oweALT 4883  fiint 5650  aceq3lem 5894  aceq5lem3 5899  aceq5lem4 5900  aceq5 5902  aceq6b 5904  kmlem1 5927  kmlem12 5938  kmlem14 5940  numthlem 5945  dominf 6052  axrrecex 6437  elimne0 6469  1re 6598  msqgt0 6797  gt0ne0 6800  recex 6876  mulcant2i 6879  divmul 6896  divcl 6901  divcan1 6909  recne0 6915  recid 6918  divrec 6922  divdir 6933  divcan3 6938  div11 6941  recrec 6952  redivcl 6978  qreccl 7453  absdiv 8111  cjdiv 8141  absgt0 8145  efseq1ex 8568  qdensere 9027  hausnei 9061  dscmet 9196  bcthlem7 9283  spwval2 9996  isfbas 10261  fipfil2 10272  hausfillim 10303  norm1exi 10755  shintcl 10927  chintcl 10929  chne0 11050  elspansn2 11123  eigre 11398  eigorth 11401  kbpj 11517  eleigvec 11518  superpos 11926  hatomic 11932  bnj168 12496  bnj922 12834  bnj1154 13438  divalglem7 13702  divalg 13706  gcdcllem1 13718  gcdcllem3 13720  isprm2lem 13774  nepss 13820  tz6.26 13913  frmin 13938  frxp 13951  infxpg 14422  osneisi 14875  efilcp 14922  filint2 14923  efilcp2 14926  cnfilca 14927  tclinf 15241  efp2 15290  dfcon2 15442  connsub 15443  t0dist 15541  ist1-2 15542  ist1-3 15543  t1sep 15546  fimax 15746  fimaxg 15747  acdcg 15750  inficl 15757  zornn0 15764  isdivrng3 16112  ispridl 16182  ismaxidl 16188  isposNEW 16773  atlatex 17013  hlsuprexch 17033  islinei 17221

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877  df-ne 2019

Copyright terms: Public domain