Theorem neeq1 1593

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 1484	. . 3 |- (A = B -> (A = C <-> B = C))
2	1	negbid 613	. 2 |- (A = B -> (-. A = C <-> -. B = C))
3		df-ne 1590	. 2 |- (A =/= C <-> -. A = C)
4		df-ne 1590	. 2 |- (B =/= C <-> -. B = C)
5	2, 3, 4	3bitr4g 557	1 |- (A = B -> (A =/= C <-> B =/= C))

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

This theorem is referenced by:  neeq1i 1595  neeq1d 1597  psseq1 2138  0inp0 2743  nnullss 2774  fri 2924  frc 2926  limeq 2966  xp11 3482  tz6.12i 3747  isofrlem 3907  f1oweALT 3912  fiint 4572  fiintOLD 4573  aceq3lem 4742  aceq5lem3 4747  aceq5lem4 4748  aceq5 4750  aceq6b 4752  kmlem1 4775  kmlem12 4786  kmlem14 4788  numthlem 4793  dominf 4915  dominfOLD 4916  axrrecex 5296  elimne0 5328  1re 5447  msqgt0t 5627  gt0ne0t 5630  recext 5696  mulcant2 5700  mulcant2OLD 5701  divmult 5719  divclt 5724  divcan1t 5732  divcan2tOLD 5734  recne0t 5739  recidt 5742  divrect 5746  divdirt 5757  divdirtOLD 5758  divcan3t 5763  div11t 5766  recrect 5778  redivclt 5802  qrecclt 6274  absdivt 6860  cjdivt 6889  absgt0t 6893  efseq1ex 7306  qdensere 7748  hausnei 7781  dscmet 7915  bcthlem7 8002  spwval2 8649  norm1ex 9117  shintclt 9289  chintclt 9291  chne0t 9412  elspansn2t 9485  eigret 9756  kbpjt 9875  eleigvect 9876  superpos 10276  hatomict 10282  fipfil2 10550  efilcp 10556  filint2 10557  efilcp2 10561  cnfilca 10562

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1472  df-ne 1590

Copyright terms: Public domain