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

Theorem neeq1i 2609
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 2607 . 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 177    = wceq 1652    =/= wne 2599
This theorem is referenced by:  neeq12i  2611  eqnetri  2616  syl5eqner  2624  rabn0  3640  exss  4419  brwitnlem  6744  en3lplem2  7664  hta  7814  kmlem3  8025  domtriomlem  8315  zorn2lem6  8374  konigthlem  8436  rpnnen1lem1  10593  rpnnen1lem2  10594  rpnnen1lem3  10595  rpnnen1lem5  10597  seqf1olem1  11355  iscyg2  15485  opprirred  15800  ptclsg  17640  iscusp2  18325  dchrptlem1  21041  dchrptlem2  21042  disjex  24025  disjexc  24026  inisegn0  27110  stoweidlem36  27753  aovnuoveq  28023  aovovn0oveq  28026  bnj1177  29313  bnj1253  29324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429  df-ne 2601
  Copyright terms: Public domain W3C validator