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

Theorem 3netr4d 2997
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 2987 . 2 (𝜑𝐶𝐵)
4 3netr4d.3 . 2 (𝜑𝐷 = 𝐵)
53, 4neeqtrrd 2994 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1620  wne 2920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1842  df-cleq 2741  df-ne 2921
This theorem is referenced by:  infpssrlem4  9291  modsumfzodifsn  12908  mgm2nsgrplem4  17580  pmtr3ncomlem1  18064  isdrng2  18930  prmirredlem  20014  uvcf1  20304  dfac14lem  21593  i1fmullem  23631  fta1glem1  24095  fta1blem  24098  plydivlem4  24221  fta1lem  24232  cubic  24746  asinlem  24765  dchrn0  25145  lgsne0  25230  perpneq  25779  axlowdimlem14  26005  cntnevol  30571  subfacp1lem5  31444  noextenddif  32098  noresle  32123  fvtransport  32416  poimirlem1  33692  poimirlem6  33697  poimirlem7  33698  dalem4  35423  cdleme35sn2aw  36217  cdleme39n  36225  cdleme41fva11  36236  trlcone  36487  hdmap1neglem1N  37588  hdmaprnlem3N  37613  stoweidlem23  40712  2zrngnmlid  42428  2zrngnmrid  42429  zlmodzxznm  42765
  Copyright terms: Public domain W3C validator