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

Theorem neeq1i 3080
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 2826 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
32necon3bii 3068 1 (𝐴𝐶𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  eqnetri  3086  exss  5347  inisegn0  5955  suppvalbr  7825  brwitnlem  8123  en3lplem2  9065  hta  9315  kmlem3  9567  domtriomlem  9853  zorn2lem6  9912  konigthlem  9979  rpnnen1lem2  12366  rpnnen1lem1  12367  rpnnen1lem3  12368  rpnnen1lem5  12370  fsuppmapnn0fiubex  13350  seqf1olem1  13399  iscyg2  18932  gsumval3lem2  18957  opprirred  19383  ptclsg  22153  iscusp2  22840  dchrptlem1  25768  dchrptlem2  25769  disjex  30271  disjexc  30272  signsply0  31721  signstfveq0a  31746  bnj1177  32176  bnj1253  32187  fin2so  34761  br2coss  35565  stoweidlem36  42202  aovnuoveq  43271  aovovn0oveq  43274  ovn0dmfun  43878  rrx2pnedifcoorneor  44601  2itscp  44666  aacllem  44800
  Copyright terms: Public domain W3C validator