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

Theorem eqnetri 3091
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 3085 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 232 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wne 3021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819  df-ne 3022
This theorem is referenced by:  eqnetrri  3092  notzfaus  5259  notzfausOLD  5260  2on0  8109  1n0  8115  noinfep  9117  card1  9391  fin23lem31  9759  s1nz  13956  bpoly4  15408  tan0  15499  resslem  16552  basendxnplusgndx  16603  plusgndxnmulrndx  16612  basendxnmulrndx  16613  slotsbhcdif  16688  rmodislmod  19638  cnfldfun  20492  xrsnsgrp  20516  matvsca  20960  ustuqtop1  22784  iaa  24848  tan4thpi  25034  ang180lem2  25320  mcubic  25357  quart1lem  25365  ex-lcm  28170  9p10ne21  28182  resvlem  30837  esumnul  31212  ballotth  31700  quad3  32816  bj-1upln0  34224  bj-2upln0  34238  bj-2upln1upl  34239  nn0rppwr  39066  sn-0ne2  39120  mncn0  39623  aaitgo  39646  stirlinglem11  42254  sec0  44761  2p2ne5  44801
  Copyright terms: Public domain W3C validator