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

Theorem eqnetrrd 3058
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
eqnetrrd.1 (𝜑𝐴 = 𝐵)
eqnetrrd.2 (𝜑𝐴𝐶)
Assertion
Ref Expression
eqnetrrd (𝜑𝐵𝐶)

Proof of Theorem eqnetrrd
StepHypRef Expression
1 eqnetrrd.1 . . 3 (𝜑𝐴 = 𝐵)
21eqcomd 2807 . 2 (𝜑𝐵 = 𝐴)
3 eqnetrrd.2 . 2 (𝜑𝐴𝐶)
42, 3eqnetrd 3057 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:  eqnetrrid  3065  3netr3d  3066  cantnflem1c  9138  eqsqrt2d  14724  tanval2  15482  tanval3  15483  tanhlt1  15509  pcadd  16219  efgsres  18860  gsumval3  19024  ablfac  19207  ablsimpgfind  19229  isdrngrd  19525  lspsneq  19891  lebnumlem3  23572  minveclem4a  24038  evthicc  24067  ioorf  24181  deg1ldgn  24698  fta1blem  24773  vieta1lem1  24910  vieta1lem2  24911  vieta1  24912  tanregt0  25135  isosctrlem2  25409  angpieqvd  25421  chordthmlem2  25423  dcubic2  25434  dquartlem1  25441  dquart  25443  asinlem  25458  atandmcj  25499  2efiatan  25508  tanatan  25509  dvatan  25525  dmgmn0  25615  dmgmdivn0  25617  lgamgulmlem2  25619  gamne0  25635  footexALT  26516  footexlem1  26517  footexlem2  26518  ttgcontlem1  26683  wlkn0  27414  fsuppcurry1  30491  fsuppcurry2  30492  bcm1n  30548  zarclssn  31230  sibfof  31712  nosep1o  33300  noetalem3  33333  finxpreclem2  34808  poimirlem9  35065  heicant  35091  heiborlem6  35253  lkrlspeqN  36466  cdlemg18d  37976  cdlemg21  37981  dibord  38454  lclkrlem2u  38822  lcfrlem9  38845  mapdindp4  39018  hdmaprnlem3uN  39146  hdmaprnlem9N  39152  fsuppind  39453  binomcxplemnotnn0  41057  dstregt0  41909  stoweidlem31  42670  stoweidlem59  42698  wallispilem4  42707  dirkertrigeqlem2  42738  fourierdlem43  42789  fourierdlem65  42810
  Copyright terms: Public domain W3C validator