Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeq1i Structured version   Visualization version   GIF version

Theorem neeq1i 3054
 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
StepHypRef Expression
1 neeq1i.1 . . 3 𝐴 = 𝐵
21eqeq1i 2806 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
32necon3bii 3042 1 (𝐴𝐶𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1538   ≠ wne 2990 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 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-ne 2991 This theorem is referenced by:  eqnetri  3060  exss  5323  inisegn0  5932  suppvalbr  7821  brwitnlem  8119  en3lplem2  9064  hta  9314  kmlem3  9567  domtriomlem  9857  zorn2lem6  9916  konigthlem  9983  rpnnen1lem2  12368  rpnnen1lem1  12369  rpnnen1lem3  12370  rpnnen1lem5  12372  fsuppmapnn0fiubex  13359  seqf1olem1  13409  iscyg2  18997  gsumval3lem2  19022  opprirred  19451  ptclsg  22223  iscusp2  22911  dchrptlem1  25851  dchrptlem2  25852  disjex  30358  disjexc  30359  signsply0  31929  signstfveq0a  31954  bnj1177  32386  bnj1253  32397  fin2so  35037  br2coss  35836  stoweidlem36  42665  aovnuoveq  43734  aovovn0oveq  43737  ovn0dmfun  44371  rrx2pnedifcoorneor  45117  2itscp  45182  aacllem  45316
 Copyright terms: Public domain W3C validator