Theorem neeq1i 2996

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

Syntax hints:   ↔ wb 209   = wceq 1543   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-ne 2933

This theorem is referenced by:  eqnetri  3002  exss  5332  inisegn0  5946  suppvalbr  7885  brwitnlem  8212  en3lplem2  9206  hta  9478  kmlem3  9731  domtriomlem  10021  zorn2lem6  10080  konigthlem  10147  rpnnen1lem2  12538  rpnnen1lem1  12539  rpnnen1lem3  12540  rpnnen1lem5  12542  fsuppmapnn0fiubex  13530  seqf1olem1  13580  iscyg2  19220  gsumval3lem2  19245  opprirred  19674  ptclsg  22466  iscusp2  23153  dchrptlem1  26099  dchrptlem2  26100  disjex  30604  disjexc  30605  signsply0  32196  signstfveq0a  32221  bnj1177  32653  bnj1253  32664  fin2so  35450  br2coss  36247  stoweidlem36  43195  aovnuoveq  44298  aovovn0oveq  44301  ovn0dmfun  44934  rrx2pnedifcoorneor  45678  2itscp  45743  aacllem  46119