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

Theorem neeq1i 3005
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 2738 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
32necon3bii 2993 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2941
This theorem is referenced by:  eqnetri  3011  exss  5421  inisegn0  6051  suppvalbr  8097  brwitnlem  8454  en3lplem2  9554  hta  9838  kmlem3  10093  domtriomlem  10383  zorn2lem6  10442  konigthlem  10509  rpnnen1lem2  12907  rpnnen1lem1  12908  rpnnen1lem3  12909  rpnnen1lem5  12911  fsuppmapnn0fiubex  13903  seqf1olem1  13953  iscyg2  19664  gsumval3lem2  19688  opprirred  20138  ptclsg  22982  iscusp2  23670  dchrptlem1  26628  dchrptlem2  26629  disjex  31556  disjexc  31557  signsply0  33220  signstfveq0a  33245  bnj1177  33675  bnj1253  33686  fin2so  36111  br2coss  36946  stoweidlem36  44363  aovnuoveq  45509  aovovn0oveq  45512  ovn0dmfun  46144  rrx2pnedifcoorneor  46888  2itscp  46953  aacllem  47334
  Copyright terms: Public domain W3C validator