Theorem neeq1i 2999

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

Syntax hints:   ↔ wb 207   = wceq 1547   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  eqnetri  3005  exss  5409  inisegn0  6057  suppvalbr  8111  brwitnlem  8439  en3lplem2  9532  hta  9819  kmlem3  10073  domtriomlem  10362  zorn2lem6  10421  konigthlem  10489  rpnnen1lem2  12925  rpnnen1lem1  12926  rpnnen1lem3  12927  rpnnen1lem5  12929  fsuppmapnn0fiubex  13952  seqf1olem1  14001  iscyg2  19855  gsumval3lem2  19879  opprirred  20400  ptclsg  23605  iscusp2  24291  dchrptlem1  27252  dchrptlem2  27253  disjex  32688  disjexc  32689  ufdprmidl  33631  constrrtlc1  33923  signsply0  34742  signstfveq0a  34767  bnj1177  35195  bnj1253  35206  vonf1owev  35343  fin2so  37981  br2coss  38902  unitscyglem3  42689  stoweidlem36  46486  aovnuoveq  47661  aovovn0oveq  47664  modm1p1ne  47846  gpg5nbgrvtx03starlem3  48568  ovn0dmfun  48654  rrx2pnedifcoorneor  49214  2itscp  49279  sectrcl  49519  invrcl  49521  isorcl  49530  aacllem  50298