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

Theorem 3netr4d 3067
 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 3057 . 2 (𝜑𝐶𝐵)
4 3netr4d.3 . 2 (𝜑𝐷 = 𝐵)
53, 4neeqtrrd 3064 1 (𝜑𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ≠ wne 2990 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-ne 2991 This theorem is referenced by:  infpssrlem4  9721  modsumfzodifsn  13311  mgm2nsgrplem4  18082  pmtr3ncomlem1  18597  isdrng2  19509  prmirredlem  20190  uvcf1  20485  dfac14lem  22226  i1fmullem  24302  fta1glem1  24770  fta1blem  24773  plydivlem4  24896  fta1lem  24907  cubic  25439  asinlem  25458  dchrn0  25838  lgsne0  25923  perpneq  26512  axlowdimlem14  26753  preimane  30437  cycpmco2lem6  30827  cycpmrn  30839  cntnevol  31601  subfacp1lem5  32545  noextenddif  33289  noresle  33314  fvtransport  33607  poimirlem1  35057  poimirlem6  35062  poimirlem7  35063  dalem4  36960  cdleme35sn2aw  37753  cdleme39n  37761  cdleme41fva11  37772  trlcone  38023  hdmaprnlem3N  39145  uvcn0  39448  stoweidlem23  42658  2zrngnmlid  44566  2zrngnmrid  44567  zlmodzxznm  44899  line2y  45162
 Copyright terms: Public domain W3C validator