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  5423  inisegn0  6069  suppvalbr  8143  brwitnlem  8471  en3lplem2  9566  hta  9850  kmlem3  10106  domtriomlem  10395  zorn2lem6  10454  konigthlem  10521  rpnnen1lem2  12936  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  fsuppmapnn0fiubex  13957  seqf1olem1  14006  iscyg2  19812  gsumval3lem2  19836  opprirred  20331  ptclsg  23502  iscusp2  24189  dchrptlem1  27175  dchrptlem2  27176  disjex  32521  disjexc  32522  ufdprmidl  33512  constrrtlc1  33722  signsply0  34542  signstfveq0a  34567  bnj1177  34996  bnj1253  35007  vonf1owev  35095  fin2so  37601  br2coss  38429  unitscyglem3  42185  stoweidlem36  46034  aovnuoveq  47192  aovovn0oveq  47195  modm1p1ne  47371  gpg5nbgrvtx03starlem3  48061  ovn0dmfun  48144  rrx2pnedifcoorneor  48705  2itscp  48770  sectrcl  49011  invrcl  49013  isorcl  49022  aacllem  49790