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

Theorem eqnetri 2476
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 2469 . 2  |-  ( A  =/=  C  <->  B  =/=  C )
41, 3mpbir 200 1  |-  A  =/= 
C
Colors of variables: wff set class
Syntax hints:    = wceq 1632    =/= wne 2459
This theorem is referenced by:  eqnetrri  2478  notzfaus  4201  2on0  6504  1n0  6510  noinfep  7376  card1  7617  fin23lem31  7985  tan0  12447  resslem  13217  iaa  19721  tan4thpi  19898  ang180lem2  20124  mcubic  20159  quart1lem  20167  ballotth  23112  esumnul  23442  bpoly4  24866  mncn0  27447  aaitgo  27470  matbas  27571  matplusg  27572  matvsca  27574  stirlinglem11  27936  sec0  28484  2p2ne5  28517
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator