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

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

Proof of Theorem neeqtrd
StepHypRef Expression
1 neeqtrd.1 . 2  |-  ( ph  ->  A  =/=  B )
2 neeqtrd.2 . . 3  |-  ( ph  ->  B  =  C )
32neeq2d 2735 . 2  |-  ( ph  ->  ( A  =/=  B  <->  A  =/=  C ) )
41, 3mpbid 210 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1395    =/= wne 2652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654
This theorem is referenced by:  neeqtrrd  2757  3netr3d  2760  xaddass2  11467  xov1plusxeqvd  11691  issubdrg  17580  ply1scln0  18458  qsssubdrg  18603  alexsublem  20669  cphsubrglem  21749  cphreccllem  21750  mdegldg  22591  tglinethru  24141  footex  24220  eupath2lem3  25105  jm2.26lem3  31105  stoweidlem36  31979  lkrpssN  34989  lnatexN  35604  lhpexle2lem  35834  lhpexle3lem  35836  cdlemg47  36563  cdlemk54  36785  tendoinvcl  36932  lcdlkreqN  37450  mapdh8ab  37605
  Copyright terms: Public domain W3C validator