Theorem neeq1i 3008

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 2996	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)

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

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  eqnetri  3014  exss  5378  inisegn0  6006  suppvalbr  7981  brwitnlem  8337  en3lplem2  9371  hta  9655  kmlem3  9908  domtriomlem  10198  zorn2lem6  10257  konigthlem  10324  rpnnen1lem2  12717  rpnnen1lem1  12718  rpnnen1lem3  12719  rpnnen1lem5  12721  fsuppmapnn0fiubex  13712  seqf1olem1  13762  iscyg2  19482  gsumval3lem2  19507  opprirred  19944  ptclsg  22766  iscusp2  23454  dchrptlem1  26412  dchrptlem2  26413  disjex  30931  disjexc  30932  signsply0  32530  signstfveq0a  32555  bnj1177  32986  bnj1253  32997  fin2so  35764  br2coss  36561  stoweidlem36  43577  aovnuoveq  44683  aovovn0oveq  44686  ovn0dmfun  45318  rrx2pnedifcoorneor  46062  2itscp  46127  aacllem  46505