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

Theorem eqnetrrd 3084
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 2827 . 2 (𝜑𝐵 = 𝐴)
3 eqnetrrd.2 . 2 (𝜑𝐴𝐶)
42, 3eqnetrd 3083 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  eqnetrrid  3091  3netr3d  3092  cantnflem1c  9139  eqsqrt2d  14718  tanval2  15476  tanval3  15477  tanhlt1  15503  pcadd  16215  efgsres  18795  gsumval3  18958  ablfac  19141  ablsimpgfind  19163  isdrngrd  19459  lspsneq  19825  lebnumlem3  23496  minveclem4a  23962  evthicc  23989  ioorf  24103  deg1ldgn  24616  fta1blem  24691  vieta1lem1  24828  vieta1lem2  24829  vieta1  24830  tanregt0  25050  isosctrlem2  25324  angpieqvd  25336  chordthmlem2  25338  dcubic2  25349  dquartlem1  25356  dquart  25358  asinlem  25373  atandmcj  25414  2efiatan  25423  tanatan  25424  dvatan  25440  dmgmn0  25531  dmgmdivn0  25533  lgamgulmlem2  25535  gamne0  25551  footexALT  26432  footexlem1  26433  footexlem2  26434  ttgcontlem1  26599  wlkn0  27330  fsuppcurry1  30388  fsuppcurry2  30389  bcm1n  30445  sibfof  31498  nosep1o  33084  noetalem3  33117  finxpreclem2  34554  poimirlem9  34783  heicant  34809  heiborlem6  34977  lkrlspeqN  36189  cdlemg18d  37699  cdlemg21  37704  dibord  38177  lclkrlem2u  38545  lcfrlem9  38568  mapdindp4  38741  hdmaprnlem3uN  38869  hdmaprnlem9N  38875  binomcxplemnotnn0  40568  dstregt0  41427  stoweidlem31  42197  stoweidlem59  42225  wallispilem4  42234  dirkertrigeqlem2  42265  fourierdlem43  42316  fourierdlem65  42337
  Copyright terms: Public domain W3C validator