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

Theorem neeqtrd 2747
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 2730 . 2  |-  ( ph  ->  ( A  =/=  B  <->  A  =/=  C ) )
41, 3mpbid 210 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    =/= wne 2648
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2650
This theorem is referenced by:  neeqtrrd  2752  3netr3d  2755  xaddass2  11325  xov1plusxeqvd  11549  issubdrg  17014  ply1scln0  17869  qsssubdrg  17998  alexsublem  19749  cphsubrglem  20829  cphreccllem  20830  mdegldg  21671  tglinethru  23182  footex  23255  eupath2lem3  23753  jm2.26lem3  29499  stoweidlem36  29980  lkrpssN  33147  lnatexN  33762  lhpexle2lem  33992  lhpexle3lem  33994  cdlemg47  34719  cdlemk54  34941  tendoinvcl  35088  lcdlkreqN  35606  mapdh8ab  35761
  Copyright terms: Public domain W3C validator