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

Theorem 3netr4d 2762
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
3netr4d.2
3netr4d.3
Assertion
Ref Expression
3netr4d

Proof of Theorem 3netr4d
StepHypRef Expression
1 3netr4d.2 . . 3
2 3netr4d.1 . . 3
31, 2eqnetrd 2750 . 2
4 3netr4d.3 . 2
53, 4neeqtrrd 2757 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  =/=wne 2652
This theorem is referenced by:  infpssrlem4  8707  mgm2nsgrplem4  16039  pmtr3ncomlem1  16498  isdrng2  17406  prmirredlem  18523  prmirredlemOLD  18526  uvcf1  18823  dfac14lem  20118  i1fmullem  22101  fta1glem1  22566  fta1blem  22569  plydivlem4  22692  fta1lem  22703  cubic  23180  asinlem  23199  dchrn0  23525  lgsne0  23608  perpneq  24091  axlowdimlem14  24258  cntnevol  28199  subfacp1lem5  28628  nofulllem4  29465  fvtransport  29682  stoweidlem23  31805  2zrngnmlid  32755  2zrngnmrid  32756  zlmodzxznm  33098  dalem4  35389  cdleme35sn2aw  36184  cdleme39n  36192  cdleme41fva11  36203  trlcone  36454  hdmap1neglem1N  37555  hdmaprnlem3N  37580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654
  Copyright terms: Public domain W3C validator