Theorem neeq1i 3003

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-ne 2939

This theorem is referenced by:  eqnetri  3009  exss  5464  inisegn0  6098  suppvalbr  8154  brwitnlem  8511  en3lplem2  9612  hta  9896  kmlem3  10151  domtriomlem  10441  zorn2lem6  10500  konigthlem  10567  rpnnen1lem2  12967  rpnnen1lem1  12968  rpnnen1lem3  12969  rpnnen1lem5  12971  fsuppmapnn0fiubex  13963  seqf1olem1  14013  iscyg2  19793  gsumval3lem2  19817  opprirred  20315  ptclsg  23341  iscusp2  24029  dchrptlem1  27001  dchrptlem2  27002  disjex  32088  disjexc  32089  signsply0  33858  signstfveq0a  33883  bnj1177  34313  bnj1253  34324  fin2so  36780  br2coss  37613  stoweidlem36  45052  aovnuoveq  46199  aovovn0oveq  46202  ovn0dmfun  46834  rrx2pnedifcoorneor  47491  2itscp  47556  aacllem  47937