Theorem neeq1i 2752

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

Syntax hints:   <-> wb 184   = wceq 1379   =/= wne 2662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664

This theorem is referenced by:  neeq12iOLD  2757  eqnetri  2763  syl5eqnerOLD  2769  rabn0  3805  exss  4710  suppvalbr  6902  brwitnlem  7154  en3lplem2  8028  hta  8311  kmlem3  8528  domtriomlem  8818  zorn2lem6  8877  konigthlem  8939  rpnnen1lem1  11204  rpnnen1lem2  11205  rpnnen1lem3  11206  rpnnen1lem5  11208  fsuppmapnn0fiubex  12061  seqf1olem1  12109  iscyg2  16673  gsumval3lem2  16698  opprirred  17132  ptclsg  19848  iscusp2  20537  dchrptlem1  23264  dchrptlem2  23265  disjex  27121  disjexc  27122  eulerpartlems  27936  signsply0  28145  signstfveq0a  28170  fin2so  29614  inisegn0  30593  stoweidlem36  31336  aovnuoveq  31743  aovovn0oveq  31746  bnj1177  33141  bnj1253  33152