MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3brtr3d Unicode version

Theorem 3brtr3d 4481
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
3brtr3d.1
3brtr3d.2
3brtr3d.3
Assertion
Ref Expression
3brtr3d

Proof of Theorem 3brtr3d
StepHypRef Expression
1 3brtr3d.1 . 2
2 3brtr3d.2 . . 3
3 3brtr3d.3 . . 3
42, 3breq12d 4465 . 2
51, 4mpbid 210 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  ofrval  6550  difsnen  7619  domunsncan  7637  phplem2  7717  infdifsn  8094  ltaddnq  9373  lemul2a  10422  xleadd2a  11475  xlemul2a  11510  monoord2  12138  expubnd  12226  bernneq2  12293  hashfun  12495  sqrlem2  13077  abs2dif2  13166  rlimdiv  13468  isercolllem1  13487  iseraltlem2  13505  iseraltlem3  13506  fsum00  13612  seqabs  13628  cvgcmp  13630  mertenslem1  13693  eftlub  13844  eirrlem  13937  bitscmp  14088  prmreclem1  14434  efgcpbl2  16775  pgpfaclem2  17133  unitgrp  17316  xblss2  20905  xmstri2  20969  mstri2  20970  xmstri  20971  mstri  20972  xmstri3  20973  mstri3  20974  msrtri  20975  nrmmetd  21095  nmtri  21145  nmoi2  21237  xrsxmet  21314  xrge0gsumle  21338  iccpnfhmeo  21445  pcorev2  21528  pi1cpbl  21544  rrxmet  21835  ovoliunlem1  21913  voliunlem3  21962  uniioombllem2  21992  dyadss  22003  dvlipcn  22395  dv11cn  22402  dvle  22408  dvfsumge  22423  dvfsumlem2  22428  dvfsumlem4  22430  dvfsum2  22435  dgrsub  22669  vieta1lem2  22707  itgulm2  22804  radcnvlem1  22808  abelthlem7  22833  efcvx  22844  logdivlti  23005  logcnlem4  23026  logccv  23044  cxple2a  23080  cxpaddlelem  23125  cxpaddle  23126  leibpi  23273  scvxcvx  23315  amgmlem  23319  logdiflbnd  23324  ftalem2  23347  ppip1le  23435  ppieq0  23450  ppiltx  23451  chpeq0  23483  chtublem  23486  chtub  23487  logexprlim  23500  perfectlem2  23505  bposlem9  23567  2sqlem8  23647  chebbnd1lem1  23654  vmadivsum  23667  rplogsumlem1  23669  dchrisum0re  23698  dchrisum0lem1  23701  selberglem2  23731  chpdifbndlem1  23738  selberg3lem1  23742  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem6  23768  pntpbnd2  23772  pntibndlem2  23776  pntlemb  23782  pntlemr  23787  pntlemo  23792  ostth2lem2  23819  ostth2lem3  23820  legso  23985  krippenlem  24067  midex  24111  opphllem3  24121  occllem  26221  nmcexi  26945  cnlnadjlem7  26992  hmopidmchi  27070  mul2lt0rlt0  27565  omndadd2d  27698  omndmul2  27702  omndmul3  27703  ogrpinvOLD  27705  ogrpinv0le  27706  ogrpaddltbi  27709  ogrpaddltrbid  27711  ogrpinv0lt  27713  isarchi3  27731  archirngz  27733  archiabllem1b  27736  gsumle  27770  orngsqr  27794  ornglmulle  27795  orngrmulle  27796  isarchiofld  27807  eulerpartlemgc  28301  dstfrvclim1  28416  lgamgulmlem2  28572  lgamgulmlem5  28575  lgambdd  28579  lgamcvg2  28597  subfaclim  28632  ovoliunnfl  30056  itg2addnclem3  30068  ftc1anclem8  30097  cntotbnd  30292  rrnmet  30325  jm2.24nn  30897  jm2.27a  30947  idomrootle  31152  binomcxplemrat  31255  binomcxplemnotnn0  31261  ioossioobi  31557  ioodvbdlimc2lem  31731  stoweidlem10  31792  stoweidlem11  31793  stoweidlem13  31795  stoweidlem14  31796  stoweidlem28  31810  stirlinglem11  31866  stirlinglem12  31867  dirkercncflem4  31888  fourierdlem4  31893  fourierdlem6  31895  fourierdlem11  31900  fourierdlem42  31931  fourierdlem51  31940  fourierdlem73  31962  fourierdlem79  31968  invisoinvl  32574  3atlem1  35207  3atlem2  35208  llncvrlpln2  35281  lplncvrlvol2  35339  dalem25  35422  dalawlem7  35601  dalawlem11  35605  cdleme22g  36074  cdlemg18b  36405  cdlemg46  36461  dia2dimlem3  36793  dihord2  36954
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator