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  12896  rpnnen1lem1  12897  rpnnen1lem3  12898  rpnnen1lem5  12900  fsuppmapnn0fiubex  13917  seqf1olem1  13966  iscyg2  19779  gsumval3lem2  19803  opprirred  20325  ptclsg  23518  iscusp2  24205  dchrptlem1  27191  dchrptlem2  27192  disjex  32554  disjexc  32555  ufdprmidl  33488  constrrtlc1  33698  signsply0  34518  signstfveq0a  34543  bnj1177  34972  bnj1253  34983  vonf1owev  35080  fin2so  37586  br2coss  38414  unitscyglem3  42170  stoweidlem36  46018  aovnuoveq  47176  aovovn0oveq  47179  modm1p1ne  47355  gpg5nbgrvtx03starlem3  48055  ovn0dmfun  48141  rrx2pnedifcoorneor  48702  2itscp  48767  sectrcl  49008  invrcl  49010  isorcl  49019  aacllem  49787