Theorem neeq1i 2989

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

Syntax hints:   ↔ wb 206   = wceq 1540   ≠ wne 2925

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  eqnetri  2995  exss  5410  inisegn0  6053  suppvalbr  8104  brwitnlem  8432  en3lplem2  9528  hta  9812  kmlem3  10066  domtriomlem  10355  zorn2lem6  10414  konigthlem  10481  rpnnen1lem2  12897  rpnnen1lem1  12898  rpnnen1lem3  12899  rpnnen1lem5  12901  fsuppmapnn0fiubex  13918  seqf1olem1  13967  iscyg2  19780  gsumval3lem2  19804  opprirred  20326  ptclsg  23519  iscusp2  24206  dchrptlem1  27192  dchrptlem2  27193  disjex  32555  disjexc  32556  ufdprmidl  33497  constrrtlc1  33718  signsply0  34538  signstfveq0a  34563  bnj1177  34992  bnj1253  35003  vonf1owev  35100  fin2so  37606  br2coss  38434  unitscyglem3  42190  stoweidlem36  46037  aovnuoveq  47195  aovovn0oveq  47198  modm1p1ne  47374  gpg5nbgrvtx03starlem3  48074  ovn0dmfun  48160  rrx2pnedifcoorneor  48721  2itscp  48786  sectrcl  49027  invrcl  49029  isorcl  49038  aacllem  49806