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

Theorem 3netr4d 3090
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 3080 . 2 (𝜑𝐶𝐵)
4 3netr4d.3 . 2 (𝜑𝐷 = 𝐵)
53, 4neeqtrrd 3087 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-ne 3014
This theorem is referenced by:  infpssrlem4  9716  modsumfzodifsn  13300  mgm2nsgrplem4  18024  pmtr3ncomlem1  18530  isdrng2  19441  prmirredlem  20568  uvcf1  20864  dfac14lem  22153  i1fmullem  24222  fta1glem1  24686  fta1blem  24689  plydivlem4  24812  fta1lem  24823  cubic  25354  asinlem  25373  dchrn0  25753  lgsne0  25838  perpneq  26427  axlowdimlem14  26668  preimane  30343  cycpmco2lem6  30700  cycpmrn  30712  cntnevol  31386  subfacp1lem5  32328  noextenddif  33072  noresle  33097  fvtransport  33390  poimirlem1  34774  poimirlem6  34779  poimirlem7  34780  dalem4  36681  cdleme35sn2aw  37474  cdleme39n  37482  cdleme41fva11  37493  trlcone  37744  hdmaprnlem3N  38866  uvcn0  39029  stoweidlem23  42185  2zrngnmlid  44148  2zrngnmrid  44149  zlmodzxznm  44480  line2y  44670
  Copyright terms: Public domain W3C validator