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 231 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941
This theorem is referenced by:  eqnetrri  3012  notzfaus  5363  2on0  8522  1n0  8526  snnen2o  9273  noinfep  9700  card1  10008  fin23lem31  10383  s1nz  14645  bpoly4  16095  tan0  16187  nn0rppwr  16598  resslemOLD  17288  basendxnmulrndx  17339  basendxnmulrndxOLD  17340  plusgndxnmulrndx  17341  slotsbhcdif  17459  slotsbhcdifOLD  17460  symgvalstructOLD  19415  cnfldfunALTOLDOLD  21393  xrsnsgrp  21420  pzriprnglem4  21495  matvscaOLD  22422  ustuqtop1  24250  iaa  26367  tan4thpi  26556  tan4thpiOLD  26557  ang180lem2  26853  mcubic  26890  quart1lem  26898  nogt01o  27741  slotsinbpsd  28449  slotslnbpsd  28450  ex-lcm  30477  9p10ne21  30489  resvlemOLD  33358  esumnul  34049  ballotth  34540  quad3  35675  bj-1upln0  37010  bj-2upln0  37024  bj-2upln1upl  37025  tan3rdpi  42386  sn-0ne2  42436  flt0  42647  flt4lem5e  42666  mncn0  43151  aaitgo  43174  mnringnmulrdOLD  44229  stirlinglem11  46099  sec0  49279  2p2ne5  49317
  Copyright terms: Public domain W3C validator