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

Theorem 3netr4d 2625
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 2613 . 2  |-  ( ph  ->  ( C  =/=  D  <->  A  =/=  B ) )
51, 4mpbird 224 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  infpssrlem4  8176  isdrng2  15835  prmirredlem  16763  dfac14lem  17639  i1fmullem  19576  fta1glem1  20078  fta1blem  20081  plydivlem4  20203  fta1lem  20214  cubic  20679  asinlem  20698  dchrn0  21024  lgsne0  21107  cntnevol  24572  subfacp1lem5  24860  nofulllem4  25625  axlowdimlem14  25859  fvtransport  25931  uvcf1  27173  stoweidlem23  27703  dalem4  30363  cdleme35sn2aw  31156  cdleme39n  31164  cdleme41fva11  31175  trlcone  31426  hdmap1neglem1N  32527  hdmaprnlem3N  32552
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