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

Theorem neeqtrri 2740
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 2454 . 2  |-  B  =  C
41, 3neeqtri 2739 1  |-  A  =/= 
C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381    =/= wne 2636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-cleq 2433  df-ne 2638
This theorem is referenced by:  cflim2  8641  pnfnemnf  11330  resslem  14562  xrsnsgrp  18322  zlmlem  18421  matbas  18782  matplusg  18783  matvsca  18785  tnglem  21020  resvlem  27687  limsucncmpi  29878  uhgrepe  32212  slotsbhcdif  32390  plusgndxnmulrndx  32459  basendxnmulrndx  32460
  Copyright terms: Public domain W3C validator