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

Theorem neeqtrri 2709
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
neeqtrr.1  |-  A  =/= 
B
neeqtrr.2  |-  C  =  B
Assertion
Ref Expression
neeqtrri  |-  A  =/= 
C

Proof of Theorem neeqtrri
StepHypRef Expression
1 neeqtrr.1 . 2  |-  A  =/= 
B
2 neeqtrr.2 . . 3  |-  C  =  B
32eqcomi 2471 . 2  |-  B  =  C
41, 3neeqtri 2708 1  |-  A  =/= 
C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455    =/= wne 2633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-cleq 2455  df-ne 2635
This theorem is referenced by:  cflim2  8724  pnfnemnf  11451  resslem  15237  slotsbhcdif  15373  xrsnsgrp  19059  zlmlem  19143  matbas  19493  matplusg  19494  matvsca  19496  tnglem  21703  resvlem  28645  limsucncmpi  31155  uhgrepe  40059  plusgndxnmulrndx  40322  basendxnmulrndx  40323
  Copyright terms: Public domain W3C validator