Theorem neeq1i 2690

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 2458	. 2 |- ( A = C <-> B = C )
3	2	necon3bii 2678	1 |- ( A =/= C <-> B =/= C )

Syntax hints:   <-> wb 188   = wceq 1446   =/= wne 2624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-cleq 2446  df-ne 2626

This theorem is referenced by:  eqnetri  2696  rabn0  3754  exss  4666  inisegn0  5203  suppvalbr  6923  brwitnlem  7214  en3lplem2  8125  hta  8373  kmlem3  8587  domtriomlem  8877  zorn2lem6  8936  konigthlem  8998  rpnnen1lem1  11297  rpnnen1lem2  11298  rpnnen1lem3  11299  rpnnen1lem5  11301  fsuppmapnn0fiubex  12211  seqf1olem1  12259  iscyg2  17529  gsumval3lem2  17552  opprirred  17942  ptclsg  20642  iscusp2  21329  dchrptlem1  24204  dchrptlem2  24205  disjex  28214  disjexc  28215  signsply0  29452  signstfveq0a  29477  bnj1177  29827  bnj1253  29838  fin2so  31944  stoweidlem36  37907  aovnuoveq  38703  aovovn0oveq  38706  ovn0dmfun  39868  aacllem  40644