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

Theorem neeq1i 3048
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 2800 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
32necon3bii 3036 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1522  wne 2984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-ne 2985
This theorem is referenced by:  eqnetri  3054  exss  5247  inisegn0  5837  suppvalbr  7685  brwitnlem  7983  en3lplem2  8922  hta  9172  kmlem3  9424  domtriomlem  9710  zorn2lem6  9769  konigthlem  9836  rpnnen1lem2  12226  rpnnen1lem1  12227  rpnnen1lem3  12228  rpnnen1lem5  12230  fsuppmapnn0fiubex  13210  seqf1olem1  13259  iscyg2  18724  gsumval3lem2  18747  opprirred  19142  ptclsg  21907  iscusp2  22594  dchrptlem1  25522  dchrptlem2  25523  disjex  30032  disjexc  30033  signsply0  31438  signstfveq0a  31463  bnj1177  31892  bnj1253  31903  fin2so  34429  br2coss  35233  stoweidlem36  41883  aovnuoveq  42926  aovovn0oveq  42929  ovn0dmfun  43533  rrx2pnedifcoorneor  44204  2itscp  44269  aacllem  44402
  Copyright terms: Public domain W3C validator