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

Theorem eqnetri 3039
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 3033 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 223 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1653  wne 2969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2790  df-ne 2970
This theorem is referenced by:  eqnetrri  3040  notzfaus  5030  2on0  7807  1n0  7813  noinfep  8805  card1  9078  fin23lem31  9451  s1nz  13623  bpoly4  15123  tan0  15214  resslem  16255  basendxnplusgndx  16307  plusgndxnmulrndx  16316  basendxnmulrndx  16317  slotsbhcdif  16392  rmodislmod  19246  cnfldfun  20077  xrsnsgrp  20101  matbas  20541  matplusg  20542  matvsca  20544  ustuqtop1  22370  iaa  24418  tan4thpi  24605  ang180lem2  24889  mcubic  24923  quart1lem  24931  ex-lcm  27835  resvlem  30339  esumnul  30618  ballotth  31108  quad3  32071  bj-1upln0  33481  bj-2upln0  33495  bj-2upln1upl  33496  mncn0  38482  aaitgo  38505  stirlinglem11  41032  sec0  43291  2p2ne5  43334
  Copyright terms: Public domain W3C validator