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

Theorem 3netr4d 2556
Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
Hypotheses
Ref Expression
3netr4d.1  |-  ( ph  ->  A  =/=  B )
3netr4d.2  |-  ( ph  ->  C  =  A )
3netr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3netr4d  |-  ( ph  ->  C  =/=  D )

Proof of Theorem 3netr4d
StepHypRef Expression
1 3netr4d.1 . 2  |-  ( ph  ->  A  =/=  B )
2 3netr4d.2 . . 3  |-  ( ph  ->  C  =  A )
3 3netr4d.3 . . 3  |-  ( ph  ->  D  =  B )
42, 3neeq12d 2544 . 2  |-  ( ph  ->  ( C  =/=  D  <->  A  =/=  B ) )
51, 4mpbird 223 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647    =/= wne 2529
This theorem is referenced by:  infpssrlem4  8079  isdrng2  15732  prmirredlem  16663  dfac14lem  17528  i1fmullem  19264  fta1glem1  19766  fta1blem  19769  plydivlem4  19891  fta1lem  19902  cubic  20367  asinlem  20386  dchrn0  20712  lgsne0  20795  subfacp1lem5  24439  nofulllem4  25185  axlowdimlem14  25410  fvtransport  25482  uvcf1  26832  dalem4  29913  cdleme35sn2aw  30706  cdleme39n  30714  cdleme41fva11  30725  trlcone  30976  hdmap1neglem1N  32077  hdmaprnlem3N  32102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-ex 1547  df-cleq 2359  df-ne 2531
  Copyright terms: Public domain W3C validator