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

Theorem 3netr4d 2754
Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 21-Nov-2019.)
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.2 . . 3  |-  ( ph  ->  C  =  A )
2 3netr4d.1 . . 3  |-  ( ph  ->  A  =/=  B )
31, 2eqnetrd 2742 . 2  |-  ( ph  ->  C  =/=  B )
4 3netr4d.3 . 2  |-  ( ph  ->  D  =  B )
53, 4neeqtrrd 2749 1  |-  ( ph  ->  C  =/=  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    =/= wne 2645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-cleq 2444  df-ne 2647
This theorem is referenced by:  infpssrlem4  8581  pmtr3ncomlem1  16093  isdrng2  16960  prmirredlem  18037  prmirredlemOLD  18040  uvcf1  18337  dfac14lem  19317  i1fmullem  21300  fta1glem1  21765  fta1blem  21768  plydivlem4  21890  fta1lem  21901  cubic  22372  asinlem  22391  dchrn0  22717  lgsne0  22800  perpneq  23245  axlowdimlem14  23348  cntnevol  26782  subfacp1lem5  27211  nofulllem4  27985  fvtransport  28202  stoweidlem23  29961  zlmodzxznm  31153  dalem4  33628  cdleme35sn2aw  34421  cdleme39n  34429  cdleme41fva11  34440  trlcone  34691  hdmap1neglem1N  35792  hdmaprnlem3N  35817
  Copyright terms: Public domain W3C validator