Theorem neeq1 1633

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 1524	. . 3 |- (A = B -> (A = C <-> B = C))
2	1	notbid 614	. 2 |- (A = B -> (-. A = C <-> -. B = C))
3		df-ne 1630	. 2 |- (A =/= C <-> -. A = C)
4		df-ne 1630	. 2 |- (B =/= C <-> -. B = C)
5	2, 3, 4	3bitr4g 558	1 |- (A = B -> (A =/= C <-> B =/= C))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   = wceq 992   =/= wne 1628

This theorem is referenced by:  neeq1i 1635  neeq1d 1637  psseq1 2187  0inp0 2812  nnullss 2846  fri 2948  frc 2950  limeq 2987  xp11 3561  tz6.12i 3852  isofrlem 4015  f1oweALT 4020  fiint 4703  aceq3lem 4878  aceq5lem3 4883  aceq5lem4 4884  aceq5 4886  aceq6b 4888  kmlem1 4911  kmlem12 4922  kmlem14 4924  numthlem 4929  dominf 5054  axrrecex 5438  elimne0 5470  1re 5589  msqgt0 5769  gt0ne0 5772  recex 5840  mulcant2i 5843  divmul 5859  divcl 5864  divcan1 5872  recne0 5878  recid 5881  divrec 5885  divdir 5896  divcan3 5901  div11 5904  recrec 5915  redivcl 5940  qreccl 6412  absdiv 7062  cjdiv 7092  absgt0 7096  efseq1ex 7511  qdensere 7961  hausnei 7994  dscmet 8129  bcthlem7 8216  spwval2 8915  norm1exi 9398  shintcl 9570  chintcl 9572  chne0 9693  elspansn2 9766  eigre 10041  eigorth 10044  kbpj 10160  eleigvec 10161  superpos 10562  hatomic 10568  osneisi 11018  fipfil2 11077  efilcp 11083  filint2 11084  efilcp2 11087  cnfilca 11088  efp2 11321  dfcon2 11501  connsub 11502  t0dist 11602  ist1-2 11603  ist1-3 11604  t1sep 11607  isfbas 11621  hausfillim 11685  fimax 11837  fimaxg 11838  acdcg 11842  inficl 11849

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511  df-ne 1630

Copyright terms: Public domain