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

Theorem eqnetri 2893
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 2887 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 221 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  eqnetrri  2894  notzfaus  4870  2on0  7614  1n0  7620  noinfep  8595  card1  8832  fin23lem31  9203  s1nz  13423  bpoly4  14834  tan0  14925  resslem  15980  basendxnplusgndx  16036  plusgndxnmulrndx  16045  basendxnmulrndx  16046  slotsbhcdif  16127  rmodislmod  18979  cnfldfun  19806  xrsnsgrp  19830  matbas  20267  matplusg  20268  matvsca  20270  ustuqtop1  22092  iaa  24125  tan4thpi  24311  ang180lem2  24585  mcubic  24619  quart1lem  24627  ex-lcm  27445  resvlem  29959  esumnul  30238  ballotth  30727  quad3  31690  bj-1upln0  33122  bj-2upln0  33136  bj-2upln1upl  33137  mncn0  38026  aaitgo  38049  stirlinglem11  40619  sec0  42829  2p2ne5  42872
  Copyright terms: Public domain W3C validator