Theorem neeq1i 2997

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

Syntax hints:   ↔ wb 206   = wceq 1540   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  eqnetri  3003  exss  5443  inisegn0  6090  suppvalbr  8168  brwitnlem  8524  en3lplem2  9632  hta  9916  kmlem3  10172  domtriomlem  10461  zorn2lem6  10520  konigthlem  10587  rpnnen1lem2  12998  rpnnen1lem1  12999  rpnnen1lem3  13000  rpnnen1lem5  13002  fsuppmapnn0fiubex  14015  seqf1olem1  14064  iscyg2  19868  gsumval3lem2  19892  opprirred  20387  ptclsg  23558  iscusp2  24245  dchrptlem1  27232  dchrptlem2  27233  disjex  32578  disjexc  32579  ufdprmidl  33561  constrrtlc1  33771  signsply0  34588  signstfveq0a  34613  bnj1177  35042  bnj1253  35053  fin2so  37636  br2coss  38461  unitscyglem3  42215  stoweidlem36  46032  aovnuoveq  47187  aovovn0oveq  47190  gpg5nbgrvtx03starlem3  48039  ovn0dmfun  48098  rrx2pnedifcoorneor  48663  2itscp  48728  aacllem  49632