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 1542   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  eqnetri  3002  exss  5415  inisegn0  6063  suppvalbr  8114  brwitnlem  8442  en3lplem2  9534  hta  9821  kmlem3  10075  domtriomlem  10364  zorn2lem6  10423  konigthlem  10491  rpnnen1lem2  12927  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  fsuppmapnn0fiubex  13954  seqf1olem1  14003  iscyg2  19857  gsumval3lem2  19881  opprirred  20402  ptclsg  23580  iscusp2  24266  dchrptlem1  27227  dchrptlem2  27228  disjex  32662  disjexc  32663  ufdprmidl  33601  constrrtlc1  33876  signsply0  34695  signstfveq0a  34720  bnj1177  35148  bnj1253  35159  vonf1owev  35290  fin2so  37928  br2coss  38849  unitscyglem3  42636  stoweidlem36  46464  aovnuoveq  47639  aovovn0oveq  47642  modm1p1ne  47824  gpg5nbgrvtx03starlem3  48546  ovn0dmfun  48632  rrx2pnedifcoorneor  49192  2itscp  49257  sectrcl  49497  invrcl  49499  isorcl  49508  aacllem  50276