Theorem neeq1i 3011

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 2999	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  eqnetri  3017  exss  5483  inisegn0  6128  suppvalbr  8205  brwitnlem  8563  en3lplem2  9682  hta  9966  kmlem3  10222  domtriomlem  10511  zorn2lem6  10570  konigthlem  10637  rpnnen1lem2  13042  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  fsuppmapnn0fiubex  14043  seqf1olem1  14092  iscyg2  19924  gsumval3lem2  19948  opprirred  20448  ptclsg  23644  iscusp2  24332  dchrptlem1  27326  dchrptlem2  27327  disjex  32614  disjexc  32615  ufdprmidl  33534  constrrtlc1  33723  signsply0  34528  signstfveq0a  34553  bnj1177  34982  bnj1253  34993  fin2so  37567  br2coss  38394  unitscyglem3  42154  stoweidlem36  45957  aovnuoveq  47106  aovovn0oveq  47109  ovn0dmfun  47879  rrx2pnedifcoorneor  48450  2itscp  48515  aacllem  48895