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

Theorem neeq1i 2887
 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 2656 . 2 (𝐴 = 𝐶𝐵 = 𝐶)
32necon3bii 2875 1 (𝐴𝐶𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   = wceq 1523   ≠ wne 2823 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824 This theorem is referenced by:  eqnetri  2893  rabn0OLD  3992  exss  4961  inisegn0  5532  suppvalbr  7344  brwitnlem  7632  en3lplem2  8550  hta  8798  kmlem3  9012  domtriomlem  9302  zorn2lem6  9361  konigthlem  9428  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  fsuppmapnn0fiubex  12832  seqf1olem1  12880  iscyg2  18330  gsumval3lem2  18353  opprirred  18748  ptclsg  21466  iscusp2  22153  dchrptlem1  25034  dchrptlem2  25035  disjex  29531  disjexc  29532  signsply0  30756  signstfveq0a  30781  bnj1177  31200  bnj1253  31211  fin2so  33526  br2coss  34333  stoweidlem36  40571  aovnuoveq  41592  aovovn0oveq  41595  ovn0dmfun  42089  aacllem  42875
 Copyright terms: Public domain W3C validator