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

Theorem eqnetri 2851
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 2845 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 219 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wne 2779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-ne 2781
This theorem is referenced by:  eqnetrri  2852  notzfaus  4761  2on0  7433  1n0  7439  noinfep  8417  card1  8654  fin23lem31  9025  s1nz  13185  bpoly4  14575  tan0  14666  resslem  15706  slotsbhcdif  15849  xrsnsgrp  19547  matbas  19980  matplusg  19981  matvsca  19983  ustuqtop1  21797  iaa  23801  tan4thpi  23987  ang180lem2  24257  mcubic  24291  quart1lem  24299  ex-lcm  26473  resvlem  28968  esumnul  29243  ballotth  29732  quad3  30624  bj-1upln0  31986  bj-2upln0  32000  bj-2upln1upl  32001  mncn0  36524  aaitgo  36547  stirlinglem11  38774  plusgndxnmulrndx  41738  basendxnmulrndx  41739  sec0  42256  2p2ne5  42309
  Copyright terms: Public domain W3C validator