Theorem neeq1i 2990

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

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

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 2702

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

This theorem is referenced by:  eqnetri  2996  exss  5426  inisegn0  6072  suppvalbr  8146  brwitnlem  8474  en3lplem2  9573  hta  9857  kmlem3  10113  domtriomlem  10402  zorn2lem6  10461  konigthlem  10528  rpnnen1lem2  12943  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  fsuppmapnn0fiubex  13964  seqf1olem1  14013  iscyg2  19819  gsumval3lem2  19843  opprirred  20338  ptclsg  23509  iscusp2  24196  dchrptlem1  27182  dchrptlem2  27183  disjex  32528  disjexc  32529  ufdprmidl  33519  constrrtlc1  33729  signsply0  34549  signstfveq0a  34574  bnj1177  35003  bnj1253  35014  vonf1owev  35102  fin2so  37608  br2coss  38436  unitscyglem3  42192  stoweidlem36  46041  aovnuoveq  47196  aovovn0oveq  47199  modm1p1ne  47375  gpg5nbgrvtx03starlem3  48065  ovn0dmfun  48148  rrx2pnedifcoorneor  48709  2itscp  48774  sectrcl  49015  invrcl  49017  isorcl  49026  aacllem  49794