Theorem neeq1i 2858

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

Syntax hints:   <-> wb 196   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  eqnetri  2864  rabn0OLD  3959  exss  4931  inisegn0  5497  suppvalbr  7299  brwitnlem  7587  en3lplem2  8512  hta  8760  kmlem3  8974  domtriomlem  9264  zorn2lem6  9323  konigthlem  9390  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  fsuppmapnn0fiubex  12792  seqf1olem1  12840  iscyg2  18284  gsumval3lem2  18307  opprirred  18702  ptclsg  21418  iscusp2  22106  dchrptlem1  24989  dchrptlem2  24990  disjex  29405  disjexc  29406  signsply0  30628  signstfveq0a  30653  bnj1177  31074  bnj1253  31085  fin2so  33396  stoweidlem36  40253  aovnuoveq  41271  aovovn0oveq  41274  ovn0dmfun  41764  aacllem  42547