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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2729  df-ne 2942

This theorem is referenced by:  eqnetri  3012  exss  5397  inisegn0  6024  suppvalbr  8030  brwitnlem  8387  en3lplem2  9449  hta  9733  kmlem3  9988  domtriomlem  10278  zorn2lem6  10337  konigthlem  10404  rpnnen1lem2  12797  rpnnen1lem1  12798  rpnnen1lem3  12799  rpnnen1lem5  12801  fsuppmapnn0fiubex  13792  seqf1olem1  13842  iscyg2  19557  gsumval3lem2  19582  opprirred  20019  ptclsg  22849  iscusp2  23537  dchrptlem1  26495  dchrptlem2  26496  disjex  31066  disjexc  31067  signsply0  32670  signstfveq0a  32695  bnj1177  33125  bnj1253  33136  fin2so  35836  br2coss  36672  stoweidlem36  43827  aovnuoveq  44948  aovovn0oveq  44951  ovn0dmfun  45583  rrx2pnedifcoorneor  46327  2itscp  46392  aacllem  46770