Theorem neeq1i 2996

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

Syntax hints:   ↔ wb 206   = wceq 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  eqnetri  3002  exss  5411  inisegn0  6057  suppvalbr  8106  brwitnlem  8434  en3lplem2  9522  hta  9809  kmlem3  10063  domtriomlem  10352  zorn2lem6  10411  konigthlem  10479  rpnnen1lem2  12890  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  fsuppmapnn0fiubex  13915  seqf1olem1  13964  iscyg2  19811  gsumval3lem2  19835  opprirred  20358  ptclsg  23559  iscusp2  24245  dchrptlem1  27231  dchrptlem2  27232  disjex  32667  disjexc  32668  ufdprmidl  33622  constrrtlc1  33889  signsply0  34708  signstfveq0a  34733  bnj1177  35162  bnj1253  35173  vonf1owev  35302  fin2so  37804  br2coss  38697  unitscyglem3  42447  stoweidlem36  46276  aovnuoveq  47433  aovovn0oveq  47436  modm1p1ne  47612  gpg5nbgrvtx03starlem3  48312  ovn0dmfun  48398  rrx2pnedifcoorneor  48958  2itscp  49023  sectrcl  49263  invrcl  49265  isorcl  49274  aacllem  50042