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

Theorem 3brtr3d 4052
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
3brtr3d.1  |-  ( ph  ->  A R B )
3brtr3d.2  |-  ( ph  ->  A  =  C )
3brtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3brtr3d  |-  ( ph  ->  C R D )

Proof of Theorem 3brtr3d
StepHypRef Expression
1 3brtr3d.1 . 2  |-  ( ph  ->  A R B )
2 3brtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
3 3brtr3d.3 . . 3  |-  ( ph  ->  B  =  D )
42, 3breq12d 4036 . 2  |-  ( ph  ->  ( A R B  <-> 
C R D ) )
51, 4mpbid 201 1  |-  ( ph  ->  C R D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  ofrval  6088  difsnen  6944  domunsncan  6962  phplem2  7041  infdifsn  7357  ltaddnq  8598  lemul2a  9611  xleadd2a  10574  xlemul2a  10609  monoord2  11077  expubnd  11162  bernneq2  11228  hashfun  11389  sqrlem2  11729  abs2dif2  11817  rlimdiv  12119  isercolllem1  12138  iseraltlem2  12155  iseraltlem3  12156  fsum00  12256  seqabs  12272  cvgcmp  12274  mertenslem1  12340  eftlub  12389  eirrlem  12482  prmreclem1  12963  efgcpbl2  15066  pgpfaclem2  15317  unitgrp  15449  xblss2  17958  xmstri2  18012  mstri2  18013  xmstri  18014  mstri  18015  xmstri3  18016  mstri3  18017  msrtri  18018  nrmmetd  18097  nmtri  18147  nmoi2  18239  xrsxmet  18315  xrge0gsumle  18338  iccpnfhmeo  18443  pcorev2  18526  pi1cpbl  18542  ovoliunlem1  18861  voliunlem3  18909  uniioombllem2  18938  dyadss  18949  dvlipcn  19341  dv11cn  19348  dvle  19354  dvfsumge  19369  dvfsumlem2  19374  dvfsumlem4  19376  dvfsum2  19381  dgrsub  19653  vieta1lem2  19691  itgulm2  19785  radcnvlem1  19789  abelthlem7  19814  efcvx  19825  logdivlti  19971  logcnlem4  19992  logccv  20010  cxple2a  20046  cxpaddlelem  20091  cxpaddle  20092  leibpi  20238  scvxcvx  20280  amgmlem  20284  ftalem2  20311  ppip1le  20399  ppieq0  20414  ppiltx  20415  chpeq0  20447  chtublem  20450  chtub  20451  logexprlim  20464  perfectlem2  20469  bposlem9  20531  2sqlem8  20611  chebbnd1lem1  20618  vmadivsum  20631  rplogsumlem1  20633  dchrisum0re  20662  dchrisum0lem1  20665  selberglem2  20695  chpdifbndlem1  20702  selberg3lem1  20706  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem6  20732  pntpbnd2  20736  pntibndlem2  20740  pntlemb  20746  pntlemr  20751  pntlemo  20756  ostth2lem2  20783  ostth2lem3  20784  occllem  21882  nmcexi  22606  cnlnadjlem7  22653  hmopidmchi  22731  subfaclim  23719  cntotbnd  26520  rrnmet  26553  jm2.24nn  27046  jm2.27a  27098  idomrootle  27511  stoweidlem10  27759  stoweidlem11  27760  stoweidlem14  27763  stoweidlem28  27777  3atlem1  29672  3atlem2  29673  llncvrlpln2  29746  lplncvrlvol2  29804  dalem25  29887  dalawlem7  30066  dalawlem11  30070  cdleme22g  30537  cdlemg18b  30868  cdlemg46  30924  dia2dimlem3  31256  dihord2  31417
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator