Theorem neeq1i 3019

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  eqnetri  3025  exss  5430  inisegn0  6095  suppvalbrOLD  8184  brwitnlem  8518  en3lplem2  9617  karden  9962  hta  9965  htaOLD  9966  kmlem3  10234  domtriomlem  10523  zorn2lem6  10582  konigthlem  10656  rpnnen1lem2  13108  rpnnen1lem1  13109  rpnnen1lem3  13110  rpnnen1lem5  13112  fsuppmapnn0fiubex  14138  seqf1olem1  14187  iscyg2  20101  gsumval3lem2  20125  opprirred  20657  ptclsg  23939  iscusp2  24625  dchrptlem1  27596  dchrptlem2  27597  disjex  33233  disjexc  33234  ufdprmidl  34119  constrrtlc1  34410  signsply0  35226  signstfveq0a  35251  bnj1177  35682  bnj1253  35693  dfscott3  35797  kardeq0  35880  vonf1wev  35955  vonf1owevOLD  35957  fin2so  38623  br2coss  39553  unitscyglem3  43340  stoweidlem36  47139  aovnuoveq  48354  aovovn0oveq  48357  modm1p1ne  48539  gpg5nbgrvtx03starlem3  49261  ovn0dmfun  49347  rrx2pnedifcoorneor  49922  2itscp  49986  sectrcl  50229  invrcl  50231  isorcl  50240  aacllem  51107