Theorem neeq1i 3024

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

Syntax hints:   ↔ wb 209   = wceq 1563   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  eqnetri  3030  exss  5435  inisegn0  6091  suppvalbr  8148  brwitnlem  8480  en3lplem2  9570  hta  9871  kmlem3  10124  domtriomlem  10414  zorn2lem6  10473  konigthlem  10541  rpnnen1lem2  12992  rpnnen1lem1  12993  rpnnen1lem3  12994  rpnnen1lem5  12996  fsuppmapnn0fiubex  14019  seqf1olem1  14068  iscyg2  19943  gsumval3lem2  19967  opprirred  20495  ptclsg  23733  iscusp2  24419  dchrptlem1  27386  dchrptlem2  27387  disjex  32847  disjexc  32848  ufdprmidl  33748  constrrtlc1  34039  signsply0  34855  signstfveq0a  34880  bnj1177  35311  bnj1253  35322  vonf1wev  35463  vonf1owevOLD  35465  fin2so  38118  br2coss  39039  unitscyglem3  42826  stoweidlem36  46608  aovnuoveq  47783  aovovn0oveq  47786  modm1p1ne  47968  gpg5nbgrvtx03starlem3  48690  ovn0dmfun  48776  rrx2pnedifcoorneor  49347  2itscp  49412  sectrcl  49651  invrcl  49653  isorcl  49662  aacllem  50430