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

Theorem eqnetrrd 2850
 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 2616 . 2 (𝜑𝐵 = 𝐴)
3 eqnetrrd.2 . 2 (𝜑𝐴𝐶)
42, 3eqnetrd 2849 1 (𝜑𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782 This theorem is referenced by:  syl5eqner  2857  3netr3d  2858  cantnflem1c  8467  eqsqrt2d  13956  tanval2  14702  tanval3  14703  tanhlt1  14729  pcadd  15431  efgsres  17974  gsumval3  18131  ablfac  18310  isdrngrd  18596  lspsneq  18943  lebnumlem3  22570  minveclem4a  23009  evthicc  23035  ioorf  23147  deg1ldgn  23657  fta1blem  23732  vieta1lem1  23869  vieta1lem2  23870  vieta1  23871  tanregt0  24089  isosctrlem2  24349  angpieqvd  24358  chordthmlem2  24360  dcubic2  24371  dquartlem1  24378  dquart  24380  asinlem  24395  atandmcj  24436  2efiatan  24445  tanatan  24446  dvatan  24462  dmgmn0  24552  dmgmdivn0  24554  lgamgulmlem2  24556  gamne0  24572  footex  25413  ttgcontlem1  25565  eupath2lem3  26506  bcm1n  28941  sibfof  29729  finxpreclem2  32403  poimirlem9  32588  heicant  32614  heiborlem6  32785  lkrlspeqN  33476  cdlemg18d  34987  cdlemg21  34992  dibord  35466  lclkrlem2u  35834  lcfrlem9  35857  mapdindp4  36030  hdmaprnlem3uN  36161  hdmaprnlem9N  36167  binomcxplemnotnn0  37577  dstregt0  38434  stoweidlem31  38924  stoweidlem59  38952  wallispilem4  38961  dirkertrigeqlem2  38992  fourierdlem43  39043  fourierdlem65  39064  1wlkn0  40825
 Copyright terms: Public domain W3C validator