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

Theorem 3netr4d 3018
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 3008 . 2 (𝜑𝐶𝐵)
4 3netr4d.3 . 2 (𝜑𝐷 = 𝐵)
53, 4neeqtrrd 3015 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wne 2940
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 2941
This theorem is referenced by:  infpssrlem4  10247  modsumfzodifsn  13855  mgm2nsgrplem4  18736  pmtr3ncomlem1  19260  isdrng2  20210  prmirredlem  20909  uvcf1  21214  dfac14lem  22984  i1fmullem  25074  fta1glem1  25546  fta1blem  25549  plydivlem4  25672  fta1lem  25683  cubic  26215  asinlem  26234  dchrn0  26614  lgsne0  26699  noextenddif  27032  noresle  27061  perpneq  27698  axlowdimlem14  27946  preimane  31632  cycpmco2lem6  32029  cycpmrn  32041  cntnevol  32884  subfacp1lem5  33835  fvtransport  34663  poimirlem1  36125  poimirlem6  36130  poimirlem7  36131  dalem4  38174  cdleme35sn2aw  38967  cdleme39n  38975  cdleme41fva11  38986  trlcone  39237  hdmaprnlem3N  40359  sticksstones2  40601  uvcn0  40773  flt0  41018  stoweidlem23  44350  2zrngnmlid  46333  2zrngnmrid  46334  zlmodzxznm  46664  line2y  46927
  Copyright terms: Public domain W3C validator