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

Theorem eqnetri 3011
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
eqnetr.1 𝐴 = 𝐵
eqnetr.2 𝐵𝐶
Assertion
Ref Expression
eqnetri 𝐴𝐶

Proof of Theorem eqnetri
StepHypRef Expression
1 eqnetr.2 . 2 𝐵𝐶
2 eqnetr.1 . . 3 𝐴 = 𝐵
32neeq1i 3005 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 230 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2941
This theorem is referenced by:  eqnetrri  3012  notzfaus  5319  2on0  8429  1n0  8435  snnen2o  9184  noinfep  9601  card1  9909  fin23lem31  10284  s1nz  14501  bpoly4  15947  tan0  16038  resslemOLD  17128  basendxnplusgndxOLD  17169  basendxnmulrndx  17181  basendxnmulrndxOLD  17182  plusgndxnmulrndx  17183  slotsbhcdif  17301  slotsbhcdifOLD  17302  symgvalstructOLD  19184  rmodislmodOLD  20406  cnfldfunALTOLD  20826  xrsnsgrp  20849  matvscaOLD  21781  ustuqtop1  23609  iaa  25701  tan4thpi  25887  ang180lem2  26176  mcubic  26213  quart1lem  26221  nogt01o  27060  slotsinbpsd  27425  slotslnbpsd  27426  ex-lcm  29444  9p10ne21  29456  resvlemOLD  32170  esumnul  32704  ballotth  33194  quad3  34315  bj-1upln0  35526  bj-2upln0  35540  bj-2upln1upl  35541  nn0rppwr  40862  sn-0ne2  40918  flt0  41018  flt4lem5e  41037  mncn0  41509  aaitgo  41532  mnringnmulrdOLD  42578  stirlinglem11  44411  sec0  47291  2p2ne5  47331
  Copyright terms: Public domain W3C validator