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 1540  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941
This theorem is referenced by:  f1ounsn  7292  infpssrlem4  10346  modsumfzodifsn  13985  mgm2nsgrplem4  18934  pmtr3ncomlem1  19491  isdrng2  20743  prmirredlem  21483  uvcf1  21812  dfac14lem  23625  i1fmullem  25729  fta1glem1  26207  fta1blem  26210  plydivlem4  26338  fta1lem  26349  cubic  26892  asinlem  26911  dchrn0  27294  lgsne0  27379  noextenddif  27713  noresle  27742  perpneq  28722  axlowdimlem14  28970  preimane  32680  cycpmco2lem6  33151  cycpmrn  33163  irngnminplynz  33755  cntnevol  34229  subfacp1lem5  35189  fvtransport  36033  poimirlem1  37628  poimirlem6  37633  poimirlem7  37634  dalem4  39667  cdleme35sn2aw  40460  cdleme39n  40468  cdleme41fva11  40479  trlcone  40730  hdmaprnlem3N  41852  sticksstones2  42148  expeq1d  42359  uvcn0  42552  flt0  42647  stoweidlem23  46038  gpg3kgrtriex  48045  2zrngnmlid  48171  2zrngnmrid  48172  zlmodzxznm  48414  line2y  48676
  Copyright terms: Public domain W3C validator