Theorem neeq1i 3007

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

Hypothesis

Ref	Expression
neeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
neeq1i	⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)

Proof of Theorem neeq1i

Step	Hyp	Ref	Expression
1		neeq1i.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqeq1i 2743	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
3	2	necon3bii 2995	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)

Syntax hints:   ↔ wb 205   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  eqnetri  3013  exss  5372  inisegn0  5995  suppvalbr  7952  brwitnlem  8299  en3lplem2  9301  hta  9586  kmlem3  9839  domtriomlem  10129  zorn2lem6  10188  konigthlem  10255  rpnnen1lem2  12646  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  fsuppmapnn0fiubex  13640  seqf1olem1  13690  iscyg2  19397  gsumval3lem2  19422  opprirred  19859  ptclsg  22674  iscusp2  23362  dchrptlem1  26317  dchrptlem2  26318  disjex  30832  disjexc  30833  signsply0  32430  signstfveq0a  32455  bnj1177  32886  bnj1253  32897  fin2so  35691  br2coss  36488  stoweidlem36  43467  aovnuoveq  44570  aovovn0oveq  44573  ovn0dmfun  45206  rrx2pnedifcoorneor  45950  2itscp  46015  aacllem  46391