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

Theorem eqnetrrd 2891
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 2657 . 2 (𝜑𝐵 = 𝐴)
3 eqnetrrd.2 . 2 (𝜑𝐴𝐶)
42, 3eqnetrd 2890 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  syl5eqner  2898  3netr3d  2899  cantnflem1c  8622  eqsqrt2d  14152  tanval2  14907  tanval3  14908  tanhlt1  14934  pcadd  15640  efgsres  18197  gsumval3  18354  ablfac  18533  isdrngrd  18821  lspsneq  19170  lebnumlem3  22809  minveclem4a  23247  evthicc  23274  ioorf  23387  deg1ldgn  23898  fta1blem  23973  vieta1lem1  24110  vieta1lem2  24111  vieta1  24112  tanregt0  24330  isosctrlem2  24594  angpieqvd  24603  chordthmlem2  24605  dcubic2  24616  dquartlem1  24623  dquart  24625  asinlem  24640  atandmcj  24681  2efiatan  24690  tanatan  24691  dvatan  24707  dmgmn0  24797  dmgmdivn0  24799  lgamgulmlem2  24801  gamne0  24817  footex  25658  ttgcontlem1  25810  wlkn0  26572  bcm1n  29682  sibfof  30530  nosep1o  31957  noetalem3  31990  finxpreclem2  33357  poimirlem9  33548  heicant  33574  heiborlem6  33745  lkrlspeqN  34776  cdlemg18d  36286  cdlemg21  36291  dibord  36765  lclkrlem2u  37133  lcfrlem9  37156  mapdindp4  37329  hdmaprnlem3uN  37460  hdmaprnlem9N  37466  binomcxplemnotnn0  38872  dstregt0  39807  stoweidlem31  40566  stoweidlem59  40594  wallispilem4  40603  dirkertrigeqlem2  40634  fourierdlem43  40685  fourierdlem65  40706
  Copyright terms: Public domain W3C validator