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

Theorem 3netr4d 2473
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 2461 . 2  |-  ( ph  ->  ( C  =/=  D  <->  A  =/=  B ) )
51, 4mpbird 223 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  infpssrlem4  7932  isdrng2  15522  prmirredlem  16446  dfac14lem  17311  i1fmullem  19049  fta1glem1  19551  fta1blem  19554  plydivlem4  19676  fta1lem  19687  cubic  20145  asinlem  20164  dchrn0  20489  lgsne0  20572  subfacp1lem5  23715  nofulllem4  24359  axlowdimlem14  24583  fvtransport  24655  uvcf1  27241  dalem4  29854  cdleme35sn2aw  30647  cdleme39n  30655  cdleme41fva11  30666  trlcone  30917  hdmap1neglem1N  32018  hdmaprnlem3N  32043
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