Theorem neeq1i 3004

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

Syntax hints:   ↔ wb 206   = wceq 1539   ≠ wne 2939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ne 2940

This theorem is referenced by:  eqnetri  3010  exss  5467  inisegn0  6115  suppvalbr  8190  brwitnlem  8546  en3lplem2  9654  hta  9938  kmlem3  10194  domtriomlem  10483  zorn2lem6  10542  konigthlem  10609  rpnnen1lem2  13020  rpnnen1lem1  13021  rpnnen1lem3  13022  rpnnen1lem5  13024  fsuppmapnn0fiubex  14034  seqf1olem1  14083  iscyg2  19901  gsumval3lem2  19925  opprirred  20423  ptclsg  23624  iscusp2  24312  dchrptlem1  27309  dchrptlem2  27310  disjex  32606  disjexc  32607  ufdprmidl  33570  constrrtlc1  33774  signsply0  34567  signstfveq0a  34592  bnj1177  35021  bnj1253  35032  fin2so  37615  br2coss  38440  unitscyglem3  42199  stoweidlem36  46056  aovnuoveq  47208  aovovn0oveq  47211  gpg5nbgrvtx03starlem3  48031  ovn0dmfun  48077  rrx2pnedifcoorneor  48642  2itscp  48707  aacllem  49375