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

Theorem eqnetri 3002
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 2996 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 221 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wne 2932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-ne 2933
This theorem is referenced by:  eqnetrri  3003  notzfaus  4989  2on0  7740  1n0  7746  noinfep  8732  card1  9004  fin23lem31  9377  s1nz  13597  bpoly4  15009  tan0  15100  resslem  16155  basendxnplusgndx  16211  plusgndxnmulrndx  16220  basendxnmulrndx  16221  slotsbhcdif  16302  rmodislmod  19153  cnfldfun  19980  xrsnsgrp  20004  matbas  20441  matplusg  20442  matvsca  20444  ustuqtop1  22266  iaa  24299  tan4thpi  24486  ang180lem2  24760  mcubic  24794  quart1lem  24802  ex-lcm  27647  resvlem  30161  esumnul  30440  ballotth  30929  quad3  31892  bj-1upln0  33321  bj-2upln0  33335  bj-2upln1upl  33336  mncn0  38229  aaitgo  38252  stirlinglem11  40822  sec0  43032  2p2ne5  43075
  Copyright terms: Public domain W3C validator