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

Theorem neeqtrd 2693
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 2684 . 2  |-  ( ph  ->  ( A  =/=  B  <->  A  =/=  C ) )
41, 3mpbid 214 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444    =/= wne 2622
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-cleq 2444  df-ne 2624
This theorem is referenced by:  neeqtrrd  2698  3netr3d  2700  xaddass2  11536  xov1plusxeqvd  11778  issubdrg  18033  ply1scln0  18884  qsssubdrg  19027  alexsublem  21059  cphsubrglem  22155  cphreccllem  22156  mdegldg  23015  tglinethru  24681  footex  24763  eupath2lem3  25707  poimirlem26  31966  lkrpssN  32729  lnatexN  33344  lhpexle2lem  33574  lhpexle3lem  33576  cdlemg47  34303  cdlemk54  34525  tendoinvcl  34672  lcdlkreqN  35190  mapdh8ab  35345  jm2.26lem3  35856  stoweidlem36  37897
  Copyright terms: Public domain W3C validator