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

Theorem 3netr4d 2858
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 2848 . 2 (𝜑𝐶𝐵)
4 3netr4d.3 . 2 (𝜑𝐷 = 𝐵)
53, 4neeqtrrd 2855 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wne 2779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-ne 2781
This theorem is referenced by:  infpssrlem4  8988  modsumfzodifsn  12562  mgm2nsgrplem4  17179  pmtr3ncomlem1  17664  isdrng2  18528  prmirredlem  19607  uvcf1  19897  dfac14lem  21177  i1fmullem  23211  fta1glem1  23673  fta1blem  23676  plydivlem4  23799  fta1lem  23810  cubic  24320  asinlem  24339  dchrn0  24719  lgsne0  24804  perpneq  25354  axlowdimlem14  25580  cntnevol  29411  subfacp1lem5  30213  nofulllem4  30897  fvtransport  31102  poimirlem1  32363  poimirlem6  32368  poimirlem7  32369  dalem4  33752  cdleme35sn2aw  34547  cdleme39n  34555  cdleme41fva11  34566  trlcone  34817  hdmap1neglem1N  35918  hdmaprnlem3N  35943  stoweidlem23  38699  2zrngnmlid  41720  2zrngnmrid  41721  zlmodzxznm  42061
  Copyright terms: Public domain W3C validator