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

Theorem 3netr4d 2598
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 2586 . 2  |-  ( ph  ->  ( C  =/=  D  <->  A  =/=  B ) )
51, 4mpbird 224 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    =/= wne 2571
This theorem is referenced by:  infpssrlem4  8146  isdrng2  15804  prmirredlem  16732  dfac14lem  17606  i1fmullem  19543  fta1glem1  20045  fta1blem  20048  plydivlem4  20170  fta1lem  20181  cubic  20646  asinlem  20665  dchrn0  20991  lgsne0  21074  cntnevol  24539  subfacp1lem5  24827  nofulllem4  25577  axlowdimlem14  25802  fvtransport  25874  uvcf1  27113  stoweidlem23  27643  dalem4  30151  cdleme35sn2aw  30944  cdleme39n  30952  cdleme41fva11  30963  trlcone  31214  hdmap1neglem1N  32315  hdmaprnlem3N  32340
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 1662  ax-8 1683  ax-11 1757  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2401  df-ne 2573
  Copyright terms: Public domain W3C validator