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

Theorem neeqtrd 2762
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 2745 . 2  |-  ( ph  ->  ( A  =/=  B  <->  A  =/=  C ) )
41, 3mpbid 210 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664
This theorem is referenced by:  neeqtrrd  2767  3netr3d  2770  xaddass2  11438  xov1plusxeqvd  11662  issubdrg  17234  ply1scln0  18100  qsssubdrg  18242  alexsublem  20276  cphsubrglem  21356  cphreccllem  21357  mdegldg  22198  tglinethru  23727  footex  23800  eupath2lem3  24652  jm2.26lem3  30547  stoweidlem36  31336  lkrpssN  33960  lnatexN  34575  lhpexle2lem  34805  lhpexle3lem  34807  cdlemg47  35532  cdlemk54  35754  tendoinvcl  35901  lcdlkreqN  36419  mapdh8ab  36574
  Copyright terms: Public domain W3C validator