Theorem neeq1i 2992

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  eqnetri  2998  exss  5403  inisegn0  6047  suppvalbr  8094  brwitnlem  8422  en3lplem2  9503  hta  9790  kmlem3  10044  domtriomlem  10333  zorn2lem6  10392  konigthlem  10459  rpnnen1lem2  12875  rpnnen1lem1  12876  rpnnen1lem3  12877  rpnnen1lem5  12879  fsuppmapnn0fiubex  13899  seqf1olem1  13948  iscyg2  19795  gsumval3lem2  19819  opprirred  20341  ptclsg  23531  iscusp2  24217  dchrptlem1  27203  dchrptlem2  27204  disjex  32570  disjexc  32571  ufdprmidl  33504  constrrtlc1  33743  signsply0  34562  signstfveq0a  34587  bnj1177  35016  bnj1253  35027  vonf1owev  35150  fin2so  37653  br2coss  38481  unitscyglem3  42236  stoweidlem36  46080  aovnuoveq  47228  aovovn0oveq  47231  modm1p1ne  47407  gpg5nbgrvtx03starlem3  48107  ovn0dmfun  48193  rrx2pnedifcoorneor  48754  2itscp  48819  sectrcl  49060  invrcl  49062  isorcl  49071  aacllem  49839