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

Theorem 3netr4d 3019
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 3009 . 2 (𝜑𝐶𝐵)
4 3netr4d.3 . 2 (𝜑𝐷 = 𝐵)
53, 4neeqtrrd 3016 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wne 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942
This theorem is referenced by:  infpssrlem4  10297  modsumfzodifsn  13905  mgm2nsgrplem4  18798  pmtr3ncomlem1  19334  isdrng2  20317  prmirredlem  21026  uvcf1  21331  dfac14lem  23103  i1fmullem  25193  fta1glem1  25665  fta1blem  25668  plydivlem4  25791  fta1lem  25802  cubic  26334  asinlem  26353  dchrn0  26733  lgsne0  26818  noextenddif  27151  noresle  27180  perpneq  27945  axlowdimlem14  28193  preimane  31873  cycpmco2lem6  32268  cycpmrn  32280  cntnevol  33164  subfacp1lem5  34113  fvtransport  34942  poimirlem1  36427  poimirlem6  36432  poimirlem7  36433  dalem4  38474  cdleme35sn2aw  39267  cdleme39n  39275  cdleme41fva11  39286  trlcone  39537  hdmaprnlem3N  40659  sticksstones2  40901  uvcn0  41062  flt0  41323  stoweidlem23  44674  2zrngnmlid  46749  2zrngnmrid  46750  zlmodzxznm  47080  line2y  47343
  Copyright terms: Public domain W3C validator