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

Theorem neeqtrd 2573
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 2565 . 2  |-  ( ph  ->  ( A  =/=  B  <->  A  =/=  C ) )
41, 3mpbid 202 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    =/= wne 2551
This theorem is referenced by:  neeqtrrd  2575  xaddass2  10762  xov1plusxeqvd  10974  issubdrg  15821  ply1scln0  16610  qsssubdrg  16682  alexsublem  17997  cphsubrglem  19012  cphreccllem  19013  mdegldg  19857  eupath2lem3  21550  jm2.26lem3  26764  stoweidlem36  27454  lkrpssN  29279  lnatexN  29894  lhpexle2lem  30124  lhpexle3lem  30126  cdlemg47  30851  cdlemk54  31073  tendoinvcl  31220  lcdlkreqN  31738  mapdh8ab  31893
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2381  df-ne 2553
  Copyright terms: Public domain W3C validator