Theorem 3brtr3d 4342

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 4326	. 2 |- ( ph -> ( A R B <-> C R D ) )
5	1, 4	mpbid 210	1 |- ( ph -> C R D )

Syntax hints:   -> wi 4   = wceq 1369   class class class wbr 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314

This theorem is referenced by:  ofrval  6351  difsnen  7414  domunsncan  7432  phplem2  7512  infdifsn  7883  ltaddnq  9164  lemul2a  10205  xleadd2a  11238  xlemul2a  11273  monoord2  11858  expubnd  11945  bernneq2  12012  hashfun  12220  sqrlem2  12754  abs2dif2  12842  rlimdiv  13144  isercolllem1  13163  iseraltlem2  13181  iseraltlem3  13182  fsum00  13282  seqabs  13298  cvgcmp  13300  mertenslem1  13365  eftlub  13414  eirrlem  13507  bitscmp  13655  prmreclem1  13998  efgcpbl2  16275  pgpfaclem2  16605  unitgrp  16781  xblss2  19999  xmstri2  20063  mstri2  20064  xmstri  20065  mstri  20066  xmstri3  20067  mstri3  20068  msrtri  20069  nrmmetd  20189  nmtri  20239  nmoi2  20331  xrsxmet  20408  xrge0gsumle  20432  iccpnfhmeo  20539  pcorev2  20622  pi1cpbl  20638  rrxmet  20929  ovoliunlem1  21007  voliunlem3  21055  uniioombllem2  21085  dyadss  21096  dvlipcn  21488  dv11cn  21495  dvle  21501  dvfsumge  21516  dvfsumlem2  21521  dvfsumlem4  21523  dvfsum2  21528  dgrsub  21761  vieta1lem2  21799  itgulm2  21896  radcnvlem1  21900  abelthlem7  21925  efcvx  21936  logdivlti  22091  logcnlem4  22112  logccv  22130  cxple2a  22166  cxpaddlelem  22211  cxpaddle  22212  leibpi  22359  scvxcvx  22401  amgmlem  22405  logdiflbnd  22410  ftalem2  22433  ppip1le  22521  ppieq0  22536  ppiltx  22537  chpeq0  22569  chtublem  22572  chtub  22573  logexprlim  22586  perfectlem2  22591  bposlem9  22653  2sqlem8  22733  chebbnd1lem1  22740  vmadivsum  22753  rplogsumlem1  22755  dchrisum0re  22784  dchrisum0lem1  22787  selberglem2  22817  chpdifbndlem1  22824  selberg3lem1  22828  pntrlog2bndlem2  22849  pntrlog2bndlem3  22850  pntrlog2bndlem6  22854  pntpbnd2  22858  pntibndlem2  22862  pntlemb  22868  pntlemr  22873  pntlemo  22878  ostth2lem2  22905  ostth2lem3  22906  krippenlem  23106  occllem  24728  nmcexi  25452  cnlnadjlem7  25499  hmopidmchi  25577  omndadd2d  26193  omndmul2  26197  omndmul3  26198  ogrpinvOLD  26200  ogrpinv0le  26201  ogrpaddltrbid  26206  ogrpinv0lt  26208  isarchi3  26226  archirngz  26228  archiabllem1b  26231  gsumle  26268  orngsqr  26294  ornglmulle  26295  orngrmulle  26296  isarchiofld  26307  eulerpartlemgc  26767  dstfrvclim1  26882  lgamgulmlem2  27038  lgamgulmlem5  27041  lgambdd  27045  lgamcvg2  27063  subfaclim  27098  ovoliunnfl  28459  itg2addnclem3  28471  ftc1anclem8  28500  cntotbnd  28721  rrnmet  28754  jm2.24nn  29328  jm2.27a  29380  idomrootle  29586  stoweidlem10  29831  stoweidlem11  29832  stoweidlem13  29834  stoweidlem14  29835  stoweidlem28  29849  stirlinglem11  29905  stirlinglem12  29906  3atlem1  33223  3atlem2  33224  llncvrlpln2  33297  lplncvrlvol2  33355  dalem25  33438  dalawlem7  33617  dalawlem11  33621  cdleme22g  34088  cdlemg18b  34419  cdlemg46  34475  dia2dimlem3  34807  dihord2  34968