Theorem neeq1i 2887

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

Syntax hints:   ↔ wb 196   = wceq 1523   ≠ wne 2823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824

This theorem is referenced by:  eqnetri  2893  rabn0OLD  3992  exss  4961  inisegn0  5532  suppvalbr  7344  brwitnlem  7632  en3lplem2  8550  hta  8798  kmlem3  9012  domtriomlem  9302  zorn2lem6  9361  konigthlem  9428  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  fsuppmapnn0fiubex  12832  seqf1olem1  12880  iscyg2  18330  gsumval3lem2  18353  opprirred  18748  ptclsg  21466  iscusp2  22153  dchrptlem1  25034  dchrptlem2  25035  disjex  29531  disjexc  29532  signsply0  30756  signstfveq0a  30781  bnj1177  31200  bnj1253  31211  fin2so  33526  br2coss  34333  stoweidlem36  40571  aovnuoveq  41592  aovovn0oveq  41595  ovn0dmfun  42089  aacllem  42875