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

Theorem neeq1i 2630
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 2628 . 2  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2ax-mp 5 1  |-  ( A  =/=  C  <->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1369    =/= wne 2618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436  df-ne 2620
This theorem is referenced by:  neeq12i  2632  eqnetri  2637  syl5eqner  2645  rabn0  3669  exss  4567  suppvalbr  6706  brwitnlem  6959  en3lplem2  7833  hta  8116  kmlem3  8333  domtriomlem  8623  zorn2lem6  8682  konigthlem  8744  rpnnen1lem1  10991  rpnnen1lem2  10992  rpnnen1lem3  10993  rpnnen1lem5  10995  seqf1olem1  11857  iscyg2  16371  gsumval3lem2  16396  opprirred  16806  ptclsg  19200  iscusp2  19889  dchrptlem1  22615  dchrptlem2  22616  disjex  25946  disjexc  25947  eulerpartlems  26755  signsply0  26964  signstfveq0a  26989  fin2so  28428  inisegn0  29408  stoweidlem36  29843  aovnuoveq  30109  aovovn0oveq  30112  fsuppmapnn0fiubex  30812  bnj1177  32009  bnj1253  32020
  Copyright terms: Public domain W3C validator