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

Theorem eqnetri 2463
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
eqnetr.1  |-  A  =  B
eqnetr.2  |-  B  =/= 
C
Assertion
Ref Expression
eqnetri  |-  A  =/= 
C

Proof of Theorem eqnetri
StepHypRef Expression
1 eqnetr.2 . 2  |-  B  =/= 
C
2 eqnetr.1 . . 3  |-  A  =  B
32neeq1i 2456 . 2  |-  ( A  =/=  C  <->  B  =/=  C )
41, 3mpbir 200 1  |-  A  =/= 
C
Colors of variables: wff set class
Syntax hints:    = wceq 1623    =/= wne 2446
This theorem is referenced by:  eqnetrri  2465  notzfaus  4185  2on0  6488  1n0  6494  noinfep  7360  card1  7601  fin23lem31  7969  tan0  12431  resslem  13201  iaa  19705  tan4thpi  19882  ang180lem2  20108  mcubic  20143  quart1lem  20151  ballotth  23096  esumnul  23427  bpoly4  24794  mncn0  27344  aaitgo  27367  matbas  27468  matplusg  27469  matvsca  27471  stirlinglem11  27833  sec0  28230  2p2ne5  28260
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