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

Theorem neeqtrri 3086
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
neeqtrr.1 𝐴𝐵
neeqtrr.2 𝐶 = 𝐵
Assertion
Ref Expression
neeqtrri 𝐴𝐶

Proof of Theorem neeqtrri
StepHypRef Expression
1 neeqtrr.1 . 2 𝐴𝐵
2 neeqtrr.2 . . 3 𝐶 = 𝐵
32eqcomi 2827 . 2 𝐵 = 𝐶
41, 3neeqtri 3085 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wne 3013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-ne 3014
This theorem is referenced by:  1one2o  8258  cflim2  9673  pnfnemnf  10684  resslem  16545  basendxnplusgndx  16596  plusgndxnmulrndx  16605  basendxnmulrndx  16606  slotsbhcdif  16681  rmodislmod  19631  cnfldfun  20485  xrsnsgrp  20509  zlmlem  20592  matvsca  20953  tnglem  23176  setsvtx  26747  resvlem  30831  limsucncmpi  33690  sn-1ne2  39036
  Copyright terms: Public domain W3C validator