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

Theorem neeq1i 2845
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 2614 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
32necon3bii 2833 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wne 2779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-ne 2781
This theorem is referenced by:  eqnetri  2851  rabn0OLD  3912  exss  4851  inisegn0  5402  suppvalbr  7163  brwitnlem  7451  en3lplem2  8372  hta  8620  kmlem3  8834  domtriomlem  9124  zorn2lem6  9183  konigthlem  9246  rpnnen1lem2  11648  rpnnen1lem1  11649  rpnnen1lem3  11650  rpnnen1lem5  11652  rpnnen1lem1OLD  11655  rpnnen1lem3OLD  11656  rpnnen1lem5OLD  11658  fsuppmapnn0fiubex  12611  seqf1olem1  12659  iscyg2  18055  gsumval3lem2  18078  opprirred  18473  ptclsg  21175  iscusp2  21863  dchrptlem1  24733  dchrptlem2  24734  disjex  28580  disjexc  28581  signsply0  29747  signstfveq0a  29772  bnj1177  30121  bnj1253  30132  fin2so  32349  stoweidlem36  38712  aovnuoveq  39704  aovovn0oveq  39707  ovn0dmfun  41535  aacllem  42298
  Copyright terms: Public domain W3C validator