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

Theorem 3netr4d 2630
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 2618 . 2  |-  ( ph  ->  ( C  =/=  D  <->  A  =/=  B ) )
51, 4mpbird 225 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    =/= wne 2601
This theorem is referenced by:  infpssrlem4  8191  isdrng2  15850  prmirredlem  16778  dfac14lem  17654  i1fmullem  19589  fta1glem1  20093  fta1blem  20096  plydivlem4  20218  fta1lem  20229  cubic  20694  asinlem  20713  dchrn0  21039  lgsne0  21122  cntnevol  24587  subfacp1lem5  24875  nofulllem4  25665  axlowdimlem14  25899  fvtransport  25971  uvcf1  27232  stoweidlem23  27762  dalem4  30536  cdleme35sn2aw  31329  cdleme39n  31337  cdleme41fva11  31348  trlcone  31599  hdmap1neglem1N  32700  hdmaprnlem3N  32725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431  df-ne 2603
  Copyright terms: Public domain W3C validator