Theorem neeq1i 2997

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

Syntax hints:   ↔ wb 206   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  eqnetri  3003  exss  5410  inisegn0  6057  suppvalbr  8107  brwitnlem  8435  en3lplem2  9525  hta  9812  kmlem3  10066  domtriomlem  10355  zorn2lem6  10414  konigthlem  10482  rpnnen1lem2  12918  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  fsuppmapnn0fiubex  13945  seqf1olem1  13994  iscyg2  19848  gsumval3lem2  19872  opprirred  20393  ptclsg  23590  iscusp2  24276  dchrptlem1  27241  dchrptlem2  27242  disjex  32677  disjexc  32678  ufdprmidl  33616  constrrtlc1  33892  signsply0  34711  signstfveq0a  34736  bnj1177  35164  bnj1253  35175  vonf1owev  35306  fin2so  37942  br2coss  38863  unitscyglem3  42650  stoweidlem36  46482  aovnuoveq  47651  aovovn0oveq  47654  modm1p1ne  47836  gpg5nbgrvtx03starlem3  48558  ovn0dmfun  48644  rrx2pnedifcoorneor  49204  2itscp  49269  sectrcl  49509  invrcl  49511  isorcl  49520  aacllem  50288