Theorem neeq1i 3025

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ne 2962

This theorem is used by:  eqnetri  3031  exss  5449  inisegn0  6105  suppvalbr  8169  brwitnlem  8501  en3lplem2  9592  karden  9898  hta  9901  htaOLD  9902  kmlem3  10155  domtriomlem  10444  zorn2lem6  10503  konigthlem  10571  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  fsuppmapnn0fiubex  14048  seqf1olem1  14097  iscyg2  19983  gsumval3lem2  20007  opprirred  20537  ptclsg  23809  iscusp2  24495  dchrptlem1  27465  dchrptlem2  27466  disjex  32974  disjexc  32975  ufdprmidl  33862  constrrtlc1  34153  signsply0  34970  signstfveq0a  34995  bnj1177  35426  bnj1253  35437  dfscott3  35537  kardeq0  35593  vonf1wev  35616  vonf1owevOLD  35618  fin2so  38299  br2coss  39218  unitscyglem3  43005  stoweidlem36  46791  aovnuoveq  47969  aovovn0oveq  47972  modm1p1ne  48154  gpg5nbgrvtx03starlem3  48876  ovn0dmfun  48962  rrx2pnedifcoorneor  49537  2itscp  49602  sectrcl  49841  invrcl  49843  isorcl  49852  aacllem  50662