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

Theorem eqnetri 2852
 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 2846 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 220 1 𝐴𝐶
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782 This theorem is referenced by:  eqnetrri  2853  notzfaus  4766  2on0  7456  1n0  7462  noinfep  8440  card1  8677  fin23lem31  9048  s1nz  13239  bpoly4  14629  tan0  14720  resslem  15760  slotsbhcdif  15903  xrsnsgrp  19601  matbas  20038  matplusg  20039  matvsca  20041  ustuqtop1  21855  iaa  23884  tan4thpi  24070  ang180lem2  24340  mcubic  24374  quart1lem  24382  ex-lcm  26707  resvlem  29162  esumnul  29437  ballotth  29926  quad3  30818  bj-1upln0  32190  bj-2upln0  32204  bj-2upln1upl  32205  mncn0  36728  aaitgo  36751  stirlinglem11  38977  plusgndxnmulrndx  41743  basendxnmulrndx  41744  sec0  42300  2p2ne5  42353
 Copyright terms: Public domain W3C validator