Theorem neeq1i 3006

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 2738	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
3	2	necon3bii 2994	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)

Syntax hints:   ↔ wb 205   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  eqnetri  3012  exss  5464  inisegn0  6098  suppvalbr  8150  brwitnlem  8507  en3lplem2  9608  hta  9892  kmlem3  10147  domtriomlem  10437  zorn2lem6  10496  konigthlem  10563  rpnnen1lem2  12961  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  fsuppmapnn0fiubex  13957  seqf1olem1  14007  iscyg2  19750  gsumval3lem2  19774  opprirred  20236  ptclsg  23119  iscusp2  23807  dchrptlem1  26767  dchrptlem2  26768  disjex  31823  disjexc  31824  signsply0  33562  signstfveq0a  33587  bnj1177  34017  bnj1253  34028  fin2so  36475  br2coss  37308  stoweidlem36  44752  aovnuoveq  45899  aovovn0oveq  45902  ovn0dmfun  46534  rrx2pnedifcoorneor  47402  2itscp  47467  aacllem  47848