Theorem neeq1i 2688

Description: Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Hypothesis

Ref	Expression
neeq1i.1	|- A = B

Assertion

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

Proof of Theorem neeq1i

Step	Hyp	Ref	Expression
1		neeq1i.1	. . 3 |- A = B
2	1	eqeq1i 2409	. 2 |- ( A = C <-> B = C )
3	2	necon3bii 2671	1 |- ( A =/= C <-> B =/= C )

Syntax hints:   <-> wb 184   = wceq 1405   =/= wne 2598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-cleq 2394  df-ne 2600

This theorem is referenced by:  neeq12iOLD  2693  eqnetri  2699  syl5eqnerOLD  2705  rabn0  3758  exss  4653  suppvalbr  6860  brwitnlem  7114  en3lplem2  7985  hta  8267  kmlem3  8484  domtriomlem  8774  zorn2lem6  8833  konigthlem  8895  rpnnen1lem1  11171  rpnnen1lem2  11172  rpnnen1lem3  11173  rpnnen1lem5  11175  fsuppmapnn0fiubex  12052  seqf1olem1  12100  iscyg2  17101  gsumval3lem2  17126  opprirred  17563  ptclsg  20300  iscusp2  20989  dchrptlem1  23812  dchrptlem2  23813  disjex  27764  disjexc  27765  signsply0  28894  signstfveq0a  28919  bnj1177  29270  bnj1253  29281  fin2so  31393  inisegn0  35332  stoweidlem36  37168  aovnuoveq  37626  aovovn0oveq  37629  ovn0dmfun  38061  aacllem  38840