Theorem 3brtr3d 4201

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

Step	Hyp	Ref	Expression
1		3brtr3d.1	. 2 |- ( ph -> A R B )
2		3brtr3d.2	. . 3 |- ( ph -> A = C )
3		3brtr3d.3	. . 3 |- ( ph -> B = D )
4	2, 3	breq12d 4185	. 2 |- ( ph -> ( A R B <-> C R D ) )
5	1, 4	mpbid 202	1 |- ( ph -> C R D )

Syntax hints:   -> wi 4   = wceq 1649   class class class wbr 4172

This theorem is referenced by:  ofrval  6274  difsnen  7149  domunsncan  7167  phplem2  7246  infdifsn  7567  ltaddnq  8807  lemul2a  9821  xleadd2a  10789  xlemul2a  10824  monoord2  11309  expubnd  11395  bernneq2  11461  hashfun  11655  sqrlem2  12004  abs2dif2  12092  rlimdiv  12394  isercolllem1  12413  iseraltlem2  12431  iseraltlem3  12432  fsum00  12532  seqabs  12548  cvgcmp  12550  mertenslem1  12616  eftlub  12665  eirrlem  12758  bitscmp  12905  prmreclem1  13239  efgcpbl2  15344  pgpfaclem2  15595  unitgrp  15727  xblss2  18385  xmstri2  18449  mstri2  18450  xmstri  18451  mstri  18452  xmstri3  18453  mstri3  18454  msrtri  18455  nrmmetd  18575  nmtri  18625  nmoi2  18717  xrsxmet  18793  xrge0gsumle  18817  iccpnfhmeo  18923  pcorev2  19006  pi1cpbl  19022  ovoliunlem1  19351  voliunlem3  19399  uniioombllem2  19428  dyadss  19439  dvlipcn  19831  dv11cn  19838  dvle  19844  dvfsumge  19859  dvfsumlem2  19864  dvfsumlem4  19866  dvfsum2  19871  dgrsub  20143  vieta1lem2  20181  itgulm2  20278  radcnvlem1  20282  abelthlem7  20307  efcvx  20318  logdivlti  20468  logcnlem4  20489  logccv  20507  cxple2a  20543  cxpaddlelem  20588  cxpaddle  20589  leibpi  20735  scvxcvx  20777  amgmlem  20781  logdiflbnd  20786  ftalem2  20809  ppip1le  20897  ppieq0  20912  ppiltx  20913  chpeq0  20945  chtublem  20948  chtub  20949  logexprlim  20962  perfectlem2  20967  bposlem9  21029  2sqlem8  21109  chebbnd1lem1  21116  vmadivsum  21129  rplogsumlem1  21131  dchrisum0re  21160  dchrisum0lem1  21163  selberglem2  21193  chpdifbndlem1  21200  selberg3lem1  21204  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem6  21230  pntpbnd2  21234  pntibndlem2  21238  pntlemb  21244  pntlemr  21249  pntlemo  21254  ostth2lem2  21281  ostth2lem3  21282  occllem  22758  nmcexi  23482  cnlnadjlem7  23529  hmopidmchi  23607  ofldsqr  24193  dstfrvclim1  24688  lgamgulmlem2  24767  lgamgulmlem5  24770  lgambdd  24774  lgamcvg2  24792  subfaclim  24827  ovoliunnfl  26147  itg2addnclem3  26157  cntotbnd  26395  rrnmet  26428  jm2.24nn  26914  jm2.27a  26966  idomrootle  27379  stoweidlem10  27626  stoweidlem11  27627  stoweidlem13  27629  stoweidlem14  27630  stoweidlem28  27644  stirlinglem11  27700  stirlinglem12  27701  3atlem1  29965  3atlem2  29966  llncvrlpln2  30039  lplncvrlvol2  30097  dalem25  30180  dalawlem7  30359  dalawlem11  30363  cdleme22g  30830  cdlemg18b  31161  cdlemg46  31217  dia2dimlem3  31549  dihord2  31710

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173