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

Theorem neeqtrri 2723
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 2435 . 2  |-  B  =  C
41, 3neeqtri 2722 1  |-  A  =/= 
C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    =/= wne 2618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-ne 2620
This theorem is referenced by:  cflim2  8693  pnfnemnf  11417  resslem  15167  slotsbhcdif  15303  xrsnsgrp  18989  zlmlem  19072  matbas  19422  matplusg  19423  matvsca  19425  tnglem  21632  resvlem  28587  limsucncmpi  31095  uhgrepe  38876  plusgndxnmulrndx  39139  basendxnmulrndx  39140
  Copyright terms: Public domain W3C validator