Theorem neeq1i 2995

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

Syntax hints:   ↔ wb 205   = wceq 1534   ≠ wne 2930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ne 2931

This theorem is referenced by:  eqnetri  3001  exss  5471  inisegn0  6110  suppvalbr  8180  brwitnlem  8539  en3lplem2  9658  hta  9942  kmlem3  10197  domtriomlem  10487  zorn2lem6  10546  konigthlem  10613  rpnnen1lem2  13015  rpnnen1lem1  13016  rpnnen1lem3  13017  rpnnen1lem5  13019  fsuppmapnn0fiubex  14014  seqf1olem1  14063  iscyg2  19882  gsumval3lem2  19906  opprirred  20406  ptclsg  23613  iscusp2  24301  dchrptlem1  27296  dchrptlem2  27297  disjex  32514  disjexc  32515  ufdprmidl  33418  signsply0  34399  signstfveq0a  34424  bnj1177  34853  bnj1253  34864  fin2so  37310  br2coss  38138  stoweidlem36  45675  aovnuoveq  46822  aovovn0oveq  46825  ovn0dmfun  47551  rrx2pnedifcoorneor  48122  2itscp  48187  aacllem  48567