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

Theorem eqnetri 2567
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 2560 . 2  |-  ( A  =/=  C  <->  B  =/=  C )
41, 3mpbir 201 1  |-  A  =/= 
C
Colors of variables: wff set class
Syntax hints:    = wceq 1649    =/= wne 2550
This theorem is referenced by:  eqnetrri  2569  notzfaus  4315  2on0  6669  1n0  6675  noinfep  7547  card1  7788  fin23lem31  8156  tan0  12679  resslem  13449  ustuqtop1  18192  iaa  20109  tan4thpi  20289  ang180lem2  20519  mcubic  20554  quart1lem  20562  esumnul  24239  ballotth  24574  bpoly4  25819  mncn0  27013  aaitgo  27036  matbas  27137  matplusg  27138  matvsca  27140  stirlinglem11  27501  sec0  27849  2p2ne5  27882
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2380  df-ne 2552
  Copyright terms: Public domain W3C validator