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

Theorem neeq1i 2995
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 2731 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
32necon3bii 2983 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1534  wne 2930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ne 2931
This theorem is referenced by:  eqnetri  3001  exss  5471  inisegn0  6110  suppvalbr  8180  brwitnlem  8539  en3lplem2  9658  hta  9942  kmlem3  10197  domtriomlem  10487  zorn2lem6  10546  konigthlem  10613  rpnnen1lem2  13015  rpnnen1lem1  13016  rpnnen1lem3  13017  rpnnen1lem5  13019  fsuppmapnn0fiubex  14014  seqf1olem1  14063  iscyg2  19882  gsumval3lem2  19906  opprirred  20406  ptclsg  23613  iscusp2  24301  dchrptlem1  27296  dchrptlem2  27297  disjex  32514  disjexc  32515  ufdprmidl  33418  signsply0  34399  signstfveq0a  34424  bnj1177  34853  bnj1253  34864  fin2so  37310  br2coss  38138  stoweidlem36  45675  aovnuoveq  46822  aovovn0oveq  46825  ovn0dmfun  47551  rrx2pnedifcoorneor  48122  2itscp  48187  aacllem  48567
  Copyright terms: Public domain W3C validator