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

Theorem 3netr4d 2859
 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 2849 . 2 (𝜑𝐶𝐵)
4 3netr4d.3 . 2 (𝜑𝐷 = 𝐵)
53, 4neeqtrrd 2856 1 (𝜑𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782 This theorem is referenced by:  infpssrlem4  9011  modsumfzodifsn  12605  mgm2nsgrplem4  17231  pmtr3ncomlem1  17716  isdrng2  18580  prmirredlem  19660  uvcf1  19950  dfac14lem  21230  i1fmullem  23267  fta1glem1  23729  fta1blem  23732  plydivlem4  23855  fta1lem  23866  cubic  24376  asinlem  24395  dchrn0  24775  lgsne0  24860  perpneq  25409  axlowdimlem14  25635  cntnevol  29618  subfacp1lem5  30420  nofulllem4  31104  fvtransport  31309  poimirlem1  32580  poimirlem6  32585  poimirlem7  32586  dalem4  33969  cdleme35sn2aw  34764  cdleme39n  34772  cdleme41fva11  34783  trlcone  35034  hdmap1neglem1N  36135  hdmaprnlem3N  36160  stoweidlem23  38916  2zrngnmlid  41739  2zrngnmrid  41740  zlmodzxznm  42080
 Copyright terms: Public domain W3C validator