Theorem neeq1i 3020

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  eqnetri  3026  exss  5431  inisegn0  6092  suppvalbr  8165  brwitnlem  8499  en3lplem2  9598  karden  9940  hta  9943  htaOLD  9944  kmlem3  10212  domtriomlem  10501  zorn2lem6  10560  konigthlem  10634  rpnnen1lem2  13086  rpnnen1lem1  13087  rpnnen1lem3  13088  rpnnen1lem5  13090  fsuppmapnn0fiubex  14115  seqf1olem1  14164  iscyg2  20076  gsumval3lem2  20100  opprirred  20632  ptclsg  23914  iscusp2  24600  dchrptlem1  27573  dchrptlem2  27574  disjex  33168  disjexc  33169  ufdprmidl  34055  constrrtlc1  34346  signsply0  35163  signstfveq0a  35188  bnj1177  35619  bnj1253  35630  dfscott3  35721  kardeq0  35797  vonf1wev  35860  vonf1owevOLD  35862  fin2so  38498  br2coss  39428  unitscyglem3  43215  stoweidlem36  46990  aovnuoveq  48205  aovovn0oveq  48208  modm1p1ne  48390  gpg5nbgrvtx03starlem3  49112  ovn0dmfun  49198  rrx2pnedifcoorneor  49772  2itscp  49837  sectrcl  50074  invrcl  50076  isorcl  50085  aacllem  50883