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

Theorem 3netr4d 3066
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 3056 . 2 (𝜑𝐶𝐵)
4 3netr4d.3 . 2 (𝜑𝐷 = 𝐵)
53, 4neeqtrrd 3063 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wne 2989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2810  df-ne 2990
This theorem is referenced by:  infpssrlem4  9423  modsumfzodifsn  12987  mgm2nsgrplem4  17633  pmtr3ncomlem1  18114  isdrng2  18981  prmirredlem  20069  uvcf1  20362  dfac14lem  21655  i1fmullem  23698  fta1glem1  24162  fta1blem  24165  plydivlem4  24288  fta1lem  24299  cubic  24813  asinlem  24832  dchrn0  25212  lgsne0  25297  perpneq  25846  axlowdimlem14  26072  cntnevol  30639  subfacp1lem5  31511  noextenddif  32164  noresle  32189  fvtransport  32482  poimirlem1  33742  poimirlem6  33747  poimirlem7  33748  dalem4  35464  cdleme35sn2aw  36257  cdleme39n  36265  cdleme41fva11  36276  trlcone  36527  hdmaprnlem3N  37649  stoweidlem23  40737  2zrngnmlid  42535  2zrngnmrid  42536  zlmodzxznm  42872
  Copyright terms: Public domain W3C validator