Theorem neeq1i 3082

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

Syntax hints:   ↔ wb 208   = wceq 1537   ≠ wne 3018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-ne 3019

This theorem is referenced by:  eqnetri  3088  exss  5357  inisegn0  5963  suppvalbr  7836  brwitnlem  8134  en3lplem2  9078  hta  9328  kmlem3  9580  domtriomlem  9866  zorn2lem6  9925  konigthlem  9992  rpnnen1lem2  12379  rpnnen1lem1  12380  rpnnen1lem3  12381  rpnnen1lem5  12383  fsuppmapnn0fiubex  13363  seqf1olem1  13412  iscyg2  19003  gsumval3lem2  19028  opprirred  19454  ptclsg  22225  iscusp2  22913  dchrptlem1  25842  dchrptlem2  25843  disjex  30344  disjexc  30345  signsply0  31823  signstfveq0a  31848  bnj1177  32280  bnj1253  32291  fin2so  34881  br2coss  35685  stoweidlem36  42328  aovnuoveq  43397  aovovn0oveq  43400  ovn0dmfun  44038  rrx2pnedifcoorneor  44710  2itscp  44775  aacllem  44909