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

Theorem 3netr4d 3093
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 3083 . 2 (𝜑𝐶𝐵)
4 3netr4d.3 . 2 (𝜑𝐷 = 𝐵)
53, 4neeqtrrd 3090 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3016
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  infpssrlem4  9717  modsumfzodifsn  13302  mgm2nsgrplem4  18026  pmtr3ncomlem1  18532  isdrng2  19443  prmirredlem  20570  uvcf1  20866  dfac14lem  22155  i1fmullem  24224  fta1glem1  24688  fta1blem  24691  plydivlem4  24814  fta1lem  24825  cubic  25354  asinlem  25373  dchrn0  25754  lgsne0  25839  perpneq  26428  axlowdimlem14  26669  preimane  30344  cycpmco2lem6  30701  cycpmrn  30713  cntnevol  31387  subfacp1lem5  32329  noextenddif  33073  noresle  33098  fvtransport  33391  poimirlem1  34775  poimirlem6  34780  poimirlem7  34781  dalem4  36683  cdleme35sn2aw  37476  cdleme39n  37484  cdleme41fva11  37495  trlcone  37746  hdmaprnlem3N  38868  uvcn0  39031  stoweidlem23  42189  2zrngnmlid  44118  2zrngnmrid  44119  zlmodzxznm  44450  line2y  44640
  Copyright terms: Public domain W3C validator