Theorem neeq1i 3020

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

Syntax hints:   ↔ wb 208   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  eqnetri  3026  exss  5429  inisegn0  6084  suppvalbr  8139  brwitnlem  8471  en3lplem2  9565  hta  9852  kmlem3  10106  domtriomlem  10396  zorn2lem6  10455  konigthlem  10523  rpnnen1lem2  12975  rpnnen1lem1  12976  rpnnen1lem3  12977  rpnnen1lem5  12979  fsuppmapnn0fiubex  14002  seqf1olem1  14051  iscyg2  19905  gsumval3lem2  19929  opprirred  20450  ptclsg  23655  iscusp2  24341  dchrptlem1  27305  dchrptlem2  27306  disjex  32741  disjexc  32742  ufdprmidl  33698  constrrtlc1  33990  signsply0  34809  signstfveq0a  34834  bnj1177  35265  bnj1253  35276  vonf1wev  35415  vonf1owevOLD  35417  fin2so  38070  br2coss  38991  unitscyglem3  42778  stoweidlem36  46574  aovnuoveq  47749  aovovn0oveq  47752  modm1p1ne  47934  gpg5nbgrvtx03starlem3  48656  ovn0dmfun  48742  rrx2pnedifcoorneor  49302  2itscp  49367  sectrcl  49607  invrcl  49609  isorcl  49618  aacllem  50386