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

Theorem 3netr4d 2900
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 2890 . 2 (𝜑𝐶𝐵)
4 3netr4d.3 . 2 (𝜑𝐷 = 𝐵)
53, 4neeqtrrd 2897 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  infpssrlem4  9166  modsumfzodifsn  12783  mgm2nsgrplem4  17455  pmtr3ncomlem1  17939  isdrng2  18805  prmirredlem  19889  uvcf1  20179  dfac14lem  21468  i1fmullem  23506  fta1glem1  23970  fta1blem  23973  plydivlem4  24096  fta1lem  24107  cubic  24621  asinlem  24640  dchrn0  25020  lgsne0  25105  perpneq  25654  axlowdimlem14  25880  cntnevol  30419  subfacp1lem5  31292  noextenddif  31946  noresle  31971  fvtransport  32264  poimirlem1  33540  poimirlem6  33545  poimirlem7  33546  dalem4  35269  cdleme35sn2aw  36063  cdleme39n  36071  cdleme41fva11  36082  trlcone  36333  hdmap1neglem1N  37434  hdmaprnlem3N  37459  stoweidlem23  40558  2zrngnmlid  42274  2zrngnmrid  42275  zlmodzxznm  42611
  Copyright terms: Public domain W3C validator