Theorem neeq1 1587

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 1478	. . 3 |- (A = B -> (A = C <-> B = C))
2	1	negbid 610	. 2 |- (A = B -> (-. A = C <-> -. B = C))
3		df-ne 1584	. 2 |- (A =/= C <-> -. A = C)
4		df-ne 1584	. 2 |- (B =/= C <-> -. B = C)
5	2, 3, 4	3bitr4g 554	1 |- (A = B -> (A =/= C <-> B =/= C))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   = wceq 954   =/= wne 1582

This theorem is referenced by:  neeq1i 1589  neeq1d 1591  psseq1 2131  0inp0 2733  nnullss 2763  fri 2913  frc 2915  limeq 2955  xp11 3468  tz6.12i 3732  isofrlem 3892  f1oweALT 3897  fiint 4540  aceq3lem 4712  aceq5lem3 4717  aceq5lem4 4718  aceq5 4720  aceq6b 4722  kmlem1 4745  kmlem12 4756  kmlem14 4758  numthlem 4763  dominf 4884  axrrecex 5264  elimne0 5296  1re 5415  msqgt0t 5597  gt0ne0t 5600  recext 5665  mulcant2 5668  divmult 5684  divclt 5689  divcan1t 5697  divcan2t 5698  recne0t 5703  recidt 5706  divrect 5710  divdirt 5721  divcan3t 5726  div11t 5729  recrect 5740  redivclt 5764  qrecclt 6219  absdivt 6803  cjdivt 6835  absgt0t 6839  efseq1ex 7256  qdensere 7701  hausnei 7734  dscmet 7870  bcthlem7 7955  spwval2 8595  norm1ex 9061  shintclt 9232  chintclt 9234  chne0t 9355  elspansn2t 9429  eigret 9701  kbpjt 9819  eleigvect 9820  superpos 10218  hatomict 10224  fipfil2 10475  efilcp 10481  filint2 10482  efilcp2 10486  cnfilca 10487

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467  df-ne 1584

Copyright terms: Public domain