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

Theorem neeq1i 2846
 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 2615 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
32necon3bii 2834 1 (𝐴𝐶𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   = wceq 1475   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782 This theorem is referenced by:  eqnetri  2852  rabn0OLD  3913  exss  4858  inisegn0  5416  suppvalbr  7186  brwitnlem  7474  en3lplem2  8395  hta  8643  kmlem3  8857  domtriomlem  9147  zorn2lem6  9206  konigthlem  9269  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  fsuppmapnn0fiubex  12654  seqf1olem1  12702  iscyg2  18107  gsumval3lem2  18130  opprirred  18525  ptclsg  21228  iscusp2  21916  dchrptlem1  24789  dchrptlem2  24790  disjex  28787  disjexc  28788  signsply0  29954  signstfveq0a  29979  bnj1177  30328  bnj1253  30339  fin2so  32566  stoweidlem36  38929  aovnuoveq  39920  aovovn0oveq  39923  ovn0dmfun  41554  aacllem  42356
 Copyright terms: Public domain W3C validator