Theorem neeq1i 2728

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

Syntax hints:   <-> wb 184   = wceq 1383   =/= wne 2638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ne 2640

This theorem is referenced by:  neeq12iOLD  2733  eqnetri  2739  syl5eqnerOLD  2745  rabn0  3791  exss  4700  suppvalbr  6907  brwitnlem  7159  en3lplem2  8035  hta  8318  kmlem3  8535  domtriomlem  8825  zorn2lem6  8884  konigthlem  8946  rpnnen1lem1  11219  rpnnen1lem2  11220  rpnnen1lem3  11221  rpnnen1lem5  11223  fsuppmapnn0fiubex  12080  seqf1olem1  12128  iscyg2  16864  gsumval3lem2  16889  opprirred  17330  ptclsg  20094  iscusp2  20783  dchrptlem1  23517  dchrptlem2  23518  disjex  27429  disjexc  27430  signsply0  28486  signstfveq0a  28511  fin2so  30016  inisegn0  30965  stoweidlem36  31772  aovnuoveq  32230  aovovn0oveq  32233  ovn0dmfun  32406  bnj1177  33930  bnj1253  33941