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

Theorem eqnetrrd 3010
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 2742 . 2 (𝜑𝐵 = 𝐴)
3 eqnetrrd.2 . 2 (𝜑𝐴𝐶)
42, 3eqnetrd 3009 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wne 2941
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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-ne 2942
This theorem is referenced by:  eqnetrrid  3017  3netr3d  3018  cantnflem1c  9619  eqsqrt2d  15245  tanval2  16007  tanval3  16008  tanhlt1  16034  pcadd  16753  efgsres  19511  gsumval3  19675  ablfac  19858  ablsimpgfind  19880  isdrngrd  20200  lspsneq  20568  lebnumlem3  24310  minveclem4a  24778  evthicc  24807  ioorf  24921  deg1ldgn  25442  fta1blem  25517  vieta1lem1  25654  vieta1lem2  25655  vieta1  25656  tanregt0  25879  isosctrlem2  26153  angpieqvd  26165  chordthmlem2  26167  dcubic2  26178  dquartlem1  26185  dquart  26187  asinlem  26202  atandmcj  26243  2efiatan  26252  tanatan  26253  dvatan  26269  dmgmn0  26359  dmgmdivn0  26361  lgamgulmlem2  26363  gamne0  26379  nosep1o  27013  noetasuplem4  27068  footexALT  27546  footexlem1  27547  footexlem2  27548  ttgcontlem1  27719  wlkn0  28455  fsuppcurry1  31525  fsuppcurry2  31526  bcm1n  31581  zarclssn  32323  sibfof  32809  finxpreclem2  35828  poimirlem9  36054  heicant  36080  heiborlem6  36242  lkrlspeqN  37600  cdlemg18d  39111  cdlemg21  39116  dibord  39589  lclkrlem2u  39957  lcfrlem9  39980  mapdindp4  40153  hdmaprnlem3uN  40281  hdmaprnlem9N  40287  fsuppind  40703  binomcxplemnotnn0  42578  dstregt0  43451  stoweidlem31  44204  stoweidlem59  44232  wallispilem4  44241  dirkertrigeqlem2  44272  fourierdlem43  44323  fourierdlem65  44344  catprs  46963
  Copyright terms: Public domain W3C validator