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

Theorem neeq1i 2456
Description: Inference for inequality. (Contributed by NM, 29-Apr-2005.)
Hypothesis
Ref Expression
neeq1i.1  |-  A  =  B
Assertion
Ref Expression
neeq1i  |-  ( A  =/=  C  <->  B  =/=  C )

Proof of Theorem neeq1i
StepHypRef Expression
1 neeq1i.1 . 2  |-  A  =  B
2 neeq1 2454 . 2  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2ax-mp 8 1  |-  ( A  =/=  C  <->  B  =/=  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    =/= wne 2446
This theorem is referenced by:  neeq12i  2458  eqnetri  2463  syl5eqner  2471  rabn0  3474  exss  4236  brwitnlem  6506  en3lplem2  7417  hta  7567  kmlem3  7778  domtriomlem  8068  zorn2lem6  8128  konigthlem  8190  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  seqf1olem1  11085  iscyg2  15169  opprirred  15484  ptclsg  17309  dchrptlem1  20503  dchrptlem2  20504  nbssntrs  26147  inisegn0  27140  stoweidlem36  27785  aovnuoveq  28051  aovovn0oveq  28054  bnj1177  29036  bnj1253  29047
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator