Theorem neeq1i 3023

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqnetri  3029  exss  5436  inisegn0  6109  suppvalbrOLD  8212  brwitnlem  8546  en3lplem2  9644  karden  9989  hta  9992  htaOLD  9993  kmlem3  10261  domtriomlem  10550  zorn2lem6  10609  konigthlem  10683  rpnnen1lem2  13135  rpnnen1lem1  13136  rpnnen1lem3  13137  rpnnen1lem5  13139  fsuppmapnn0fiubex  14165  seqf1olem1  14214  iscyg2  20129  gsumval3lem2  20153  opprirred  20685  ptclsg  23967  iscusp2  24653  dchrptlem1  27624  dchrptlem2  27625  disjex  33261  disjexc  33262  ufdprmidl  34157  constrrtlc1  34447  signsply0  35263  signstfveq0a  35288  bnj1177  35719  bnj1253  35730  dfscott3  35840  kardeq0  35937  vonf1wev  36049  vonf1owevOLD  36051  fin2so  38735  br2coss  39663  unitscyglem3  43450  stoweidlem36  47261  aovnuoveq  48476  aovovn0oveq  48479  modm1p1ne  48661  gpg5nbgrvtx03starlem3  49383  ovn0dmfun  49469  rrx2pnedifcoorneor  50044  2itscp  50108  sectrcl  50351  invrcl  50353  isorcl  50362  aacllem  51251