Theorem neeq1i 3021

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

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

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 2155  ax-ext 2734

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

This theorem is used by:  eqnetri  3027  exss  5442  inisegn0  6098  suppvalbr  8166  brwitnlem  8498  en3lplem2  9596  karden  9902  hta  9905  htaOLD  9906  kmlem3  10159  domtriomlem  10448  zorn2lem6  10507  konigthlem  10581  rpnnen1lem2  13031  rpnnen1lem1  13032  rpnnen1lem3  13033  rpnnen1lem5  13035  fsuppmapnn0fiubex  14060  seqf1olem1  14109  iscyg2  20015  gsumval3lem2  20039  opprirred  20569  ptclsg  23847  iscusp2  24533  dchrptlem1  27508  dchrptlem2  27509  disjex  33073  disjexc  33074  ufdprmidl  33959  constrrtlc1  34250  signsply0  35067  signstfveq0a  35092  bnj1177  35523  bnj1253  35534  dfscott3  35634  kardeq0  35690  vonf1wev  35713  vonf1owevOLD  35715  fin2so  38369  br2coss  39284  unitscyglem3  43071  stoweidlem36  46872  aovnuoveq  48087  aovovn0oveq  48090  modm1p1ne  48272  gpg5nbgrvtx03starlem3  48994  ovn0dmfun  49080  rrx2pnedifcoorneor  49654  2itscp  49719  sectrcl  49956  invrcl  49958  isorcl  49967  aacllem  50780