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

Theorem 3brtr3d 4241
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 4225 . 2  |-  ( ph  ->  ( A R B  <-> 
C R D ) )
51, 4mpbid 202 1  |-  ( ph  ->  C R D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   class class class wbr 4212
This theorem is referenced by:  ofrval  6315  difsnen  7190  domunsncan  7208  phplem2  7287  infdifsn  7611  ltaddnq  8851  lemul2a  9865  xleadd2a  10833  xlemul2a  10868  monoord2  11354  expubnd  11440  bernneq2  11506  hashfun  11700  sqrlem2  12049  abs2dif2  12137  rlimdiv  12439  isercolllem1  12458  iseraltlem2  12476  iseraltlem3  12477  fsum00  12577  seqabs  12593  cvgcmp  12595  mertenslem1  12661  eftlub  12710  eirrlem  12803  bitscmp  12950  prmreclem1  13284  efgcpbl2  15389  pgpfaclem2  15640  unitgrp  15772  xblss2  18432  xmstri2  18496  mstri2  18497  xmstri  18498  mstri  18499  xmstri3  18500  mstri3  18501  msrtri  18502  nrmmetd  18622  nmtri  18672  nmoi2  18764  xrsxmet  18840  xrge0gsumle  18864  iccpnfhmeo  18970  pcorev2  19053  pi1cpbl  19069  ovoliunlem1  19398  voliunlem3  19446  uniioombllem2  19475  dyadss  19486  dvlipcn  19878  dv11cn  19885  dvle  19891  dvfsumge  19906  dvfsumlem2  19911  dvfsumlem4  19913  dvfsum2  19918  dgrsub  20190  vieta1lem2  20228  itgulm2  20325  radcnvlem1  20329  abelthlem7  20354  efcvx  20365  logdivlti  20515  logcnlem4  20536  logccv  20554  cxple2a  20590  cxpaddlelem  20635  cxpaddle  20636  leibpi  20782  scvxcvx  20824  amgmlem  20828  logdiflbnd  20833  ftalem2  20856  ppip1le  20944  ppieq0  20959  ppiltx  20960  chpeq0  20992  chtublem  20995  chtub  20996  logexprlim  21009  perfectlem2  21014  bposlem9  21076  2sqlem8  21156  chebbnd1lem1  21163  vmadivsum  21176  rplogsumlem1  21178  dchrisum0re  21207  dchrisum0lem1  21210  selberglem2  21240  chpdifbndlem1  21247  selberg3lem1  21251  pntrlog2bndlem2  21272  pntrlog2bndlem3  21273  pntrlog2bndlem6  21277  pntpbnd2  21281  pntibndlem2  21285  pntlemb  21291  pntlemr  21296  pntlemo  21301  ostth2lem2  21328  ostth2lem3  21329  occllem  22805  nmcexi  23529  cnlnadjlem7  23576  hmopidmchi  23654  ofldsqr  24240  dstfrvclim1  24735  lgamgulmlem2  24814  lgamgulmlem5  24817  lgambdd  24821  lgamcvg2  24839  subfaclim  24874  ovoliunnfl  26248  itg2addnclem3  26258  ftc1anclem8  26287  cntotbnd  26505  rrnmet  26538  jm2.24nn  27024  jm2.27a  27076  idomrootle  27488  stoweidlem10  27735  stoweidlem11  27736  stoweidlem13  27738  stoweidlem14  27739  stoweidlem28  27753  stirlinglem11  27809  stirlinglem12  27810  3atlem1  30280  3atlem2  30281  llncvrlpln2  30354  lplncvrlvol2  30412  dalem25  30495  dalawlem7  30674  dalawlem11  30678  cdleme22g  31145  cdlemg18b  31476  cdlemg46  31532  dia2dimlem3  31864  dihord2  32025
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213
  Copyright terms: Public domain W3C validator