Theorem neeq1i 2993

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

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

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 2705

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

This theorem is referenced by:  eqnetri  2999  exss  5406  inisegn0  6051  suppvalbr  8100  brwitnlem  8428  en3lplem2  9510  hta  9797  kmlem3  10051  domtriomlem  10340  zorn2lem6  10399  konigthlem  10466  rpnnen1lem2  12877  rpnnen1lem1  12878  rpnnen1lem3  12879  rpnnen1lem5  12881  fsuppmapnn0fiubex  13901  seqf1olem1  13950  iscyg2  19796  gsumval3lem2  19820  opprirred  20342  ptclsg  23531  iscusp2  24217  dchrptlem1  27203  dchrptlem2  27204  disjex  32574  disjexc  32575  ufdprmidl  33513  constrrtlc1  33766  signsply0  34585  signstfveq0a  34610  bnj1177  35039  bnj1253  35050  vonf1owev  35173  fin2so  37668  br2coss  38561  unitscyglem3  42311  stoweidlem36  46159  aovnuoveq  47316  aovovn0oveq  47319  modm1p1ne  47495  gpg5nbgrvtx03starlem3  48195  ovn0dmfun  48281  rrx2pnedifcoorneor  48842  2itscp  48907  sectrcl  49148  invrcl  49150  isorcl  49159  aacllem  49927