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

Theorem neeqtrd 2468
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 2460 . 2  |-  ( ph  ->  ( A  =/=  B  <->  A  =/=  C ) )
41, 3mpbid 201 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  neeqtrrd  2470  xaddass2  10570  xov1plusxeqvd  10780  issubdrg  15570  ply1scln0  16366  qsssubdrg  16431  alexsublem  17738  cphsubrglem  18613  cphreccllem  18614  mdegldg  19452  eupath2lem3  23903  jm2.26lem3  27094  lkrpssN  29353  lnatexN  29968  lhpexle2lem  30198  lhpexle3lem  30200  cdlemg47  30925  cdlemk54  31147  tendoinvcl  31294  lcdlkreqN  31812  mapdh8ab  31967
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator