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

Theorem neeq1i 2742
 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 2464 . 2
32necon3bii 2725 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  =wceq 1395  =/=wne 2652 This theorem is referenced by:  neeq12iOLD  2747  eqnetri  2753  syl5eqnerOLD  2759  rabn0  3805  exss  4715  suppvalbr  6922  brwitnlem  7176  en3lplem2  8053  hta  8336  kmlem3  8553  domtriomlem  8843  zorn2lem6  8902  konigthlem  8964  rpnnen1lem1  11237  rpnnen1lem2  11238  rpnnen1lem3  11239  rpnnen1lem5  11241  fsuppmapnn0fiubex  12098  seqf1olem1  12146  iscyg2  16885  gsumval3lem2  16910  opprirred  17351  ptclsg  20116  iscusp2  20805  dchrptlem1  23539  dchrptlem2  23540  disjex  27451  disjexc  27452  signsply0  28508  signstfveq0a  28533  fin2so  30040  inisegn0  30989  stoweidlem36  31818  aovnuoveq  32276  aovovn0oveq  32279  ovn0dmfun  32452  aacllem  33216  bnj1177  34062  bnj1253  34073 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654
 Copyright terms: Public domain W3C validator