Theorem neeq1i 3022

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 3010	1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)

Syntax hints:   ↔ wb 209   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  eqnetri  3028  exss  5446  inisegn0  6102  suppvalbr  8161  brwitnlem  8493  en3lplem2  9583  hta  9884  kmlem3  10137  domtriomlem  10427  zorn2lem6  10486  konigthlem  10554  rpnnen1lem2  13002  rpnnen1lem1  13003  rpnnen1lem3  13004  rpnnen1lem5  13006  fsuppmapnn0fiubex  14030  seqf1olem1  14079  iscyg2  19953  gsumval3lem2  19977  opprirred  20505  ptclsg  23753  iscusp2  24439  dchrptlem1  27406  dchrptlem2  27407  disjex  32915  disjexc  32916  ufdprmidl  33809  constrrtlc1  34100  signsply0  34916  signstfveq0a  34941  bnj1177  35372  bnj1253  35383  dfscott3  35490  kardeq0  35547  vonf1wev  35570  vonf1owevOLD  35572  fin2so  38236  br2coss  39155  unitscyglem3  42942  stoweidlem36  46730  aovnuoveq  47905  aovovn0oveq  47908  modm1p1ne  48090  gpg5nbgrvtx03starlem3  48812  ovn0dmfun  48898  rrx2pnedifcoorneor  49473  2itscp  49538  sectrcl  49777  invrcl  49779  isorcl  49788  aacllem  50578