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

Theorem 3netr4d 2579
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 2567 . 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 2552
This theorem is referenced by:  infpssrlem4  8121  isdrng2  15774  prmirredlem  16698  dfac14lem  17572  i1fmullem  19455  fta1glem1  19957  fta1blem  19960  plydivlem4  20082  fta1lem  20093  cubic  20558  asinlem  20577  dchrn0  20903  lgsne0  20986  cntnevol  24378  subfacp1lem5  24651  nofulllem4  25385  axlowdimlem14  25610  fvtransport  25682  uvcf1  26912  stoweidlem23  27442  dalem4  29781  cdleme35sn2aw  30574  cdleme39n  30582  cdleme41fva11  30593  trlcone  30844  hdmap1neglem1N  31945  hdmaprnlem3N  31970
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 1661  ax-8 1682  ax-11 1753  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2382  df-ne 2554
  Copyright terms: Public domain W3C validator