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

Theorem neeqtrd 2620
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 2612 . 2  |-  ( ph  ->  ( A  =/=  B  <->  A  =/=  C ) )
41, 3mpbid 202 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  neeqtrrd  2622  xaddass2  10821  xov1plusxeqvd  11033  issubdrg  15885  ply1scln0  16674  qsssubdrg  16750  alexsublem  18067  cphsubrglem  19132  cphreccllem  19133  mdegldg  19981  eupath2lem3  21693  jm2.26lem3  27053  stoweidlem36  27742  lkrpssN  29888  lnatexN  30503  lhpexle2lem  30733  lhpexle3lem  30735  cdlemg47  31460  cdlemk54  31682  tendoinvcl  31829  lcdlkreqN  32347  mapdh8ab  32502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428  df-ne 2600
  Copyright terms: Public domain W3C validator