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

Theorem neeqtrd 2481
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 2473 . 2  |-  ( ph  ->  ( A  =/=  B  <->  A  =/=  C ) )
41, 3mpbid 201 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  neeqtrrd  2483  xaddass2  10586  xov1plusxeqvd  10796  issubdrg  15586  ply1scln0  16382  qsssubdrg  16447  alexsublem  17754  cphsubrglem  18629  cphreccllem  18630  mdegldg  19468  eupath2lem3  23918  jm2.26lem3  27197  lkrpssN  29975  lnatexN  30590  lhpexle2lem  30820  lhpexle3lem  30822  cdlemg47  31547  cdlemk54  31769  tendoinvcl  31916  lcdlkreqN  32434  mapdh8ab  32589
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator