Theorem neeq1i 2997

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

Syntax hints:   ↔ wb 206   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  eqnetri  3003  exss  5418  inisegn0  6065  suppvalbr  8116  brwitnlem  8444  en3lplem2  9534  hta  9821  kmlem3  10075  domtriomlem  10364  zorn2lem6  10423  konigthlem  10491  rpnnen1lem2  12902  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  fsuppmapnn0fiubex  13927  seqf1olem1  13976  iscyg2  19823  gsumval3lem2  19847  opprirred  20370  ptclsg  23571  iscusp2  24257  dchrptlem1  27243  dchrptlem2  27244  disjex  32678  disjexc  32679  ufdprmidl  33633  constrrtlc1  33909  signsply0  34728  signstfveq0a  34753  bnj1177  35181  bnj1253  35192  vonf1owev  35321  fin2so  37852  br2coss  38773  unitscyglem3  42561  stoweidlem36  46388  aovnuoveq  47545  aovovn0oveq  47548  modm1p1ne  47724  gpg5nbgrvtx03starlem3  48424  ovn0dmfun  48510  rrx2pnedifcoorneor  49070  2itscp  49135  sectrcl  49375  invrcl  49377  isorcl  49386  aacllem  50154