Theorem neeq1i 3048

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

Syntax hints:   ↔ wb 207   = wceq 1522   ≠ wne 2984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-ne 2985

This theorem is referenced by:  eqnetri  3054  exss  5247  inisegn0  5837  suppvalbr  7685  brwitnlem  7983  en3lplem2  8922  hta  9172  kmlem3  9424  domtriomlem  9710  zorn2lem6  9769  konigthlem  9836  rpnnen1lem2  12226  rpnnen1lem1  12227  rpnnen1lem3  12228  rpnnen1lem5  12230  fsuppmapnn0fiubex  13210  seqf1olem1  13259  iscyg2  18724  gsumval3lem2  18747  opprirred  19142  ptclsg  21907  iscusp2  22594  dchrptlem1  25522  dchrptlem2  25523  disjex  30032  disjexc  30033  signsply0  31438  signstfveq0a  31463  bnj1177  31892  bnj1253  31903  fin2so  34429  br2coss  35233  stoweidlem36  41883  aovnuoveq  42926  aovovn0oveq  42929  ovn0dmfun  43533  rrx2pnedifcoorneor  44204  2itscp  44269  aacllem  44402