Theorem 3brtr3d 4309

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

Syntax hints:   -> wi 4   = wceq 1362   class class class wbr 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281

This theorem is referenced by:  ofrval  6319  difsnen  7381  domunsncan  7399  phplem2  7479  infdifsn  7850  ltaddnq  9130  lemul2a  10171  xleadd2a  11204  xlemul2a  11239  monoord2  11820  expubnd  11907  bernneq2  11974  hashfun  12182  sqrlem2  12716  abs2dif2  12804  rlimdiv  13106  isercolllem1  13125  iseraltlem2  13143  iseraltlem3  13144  fsum00  13243  seqabs  13259  cvgcmp  13261  mertenslem1  13326  eftlub  13375  eirrlem  13468  bitscmp  13616  prmreclem1  13959  efgcpbl2  16233  pgpfaclem2  16556  unitgrp  16692  xblss2  19818  xmstri2  19882  mstri2  19883  xmstri  19884  mstri  19885  xmstri3  19886  mstri3  19887  msrtri  19888  nrmmetd  20008  nmtri  20058  nmoi2  20150  xrsxmet  20227  xrge0gsumle  20251  iccpnfhmeo  20358  pcorev2  20441  pi1cpbl  20457  rrxmet  20748  ovoliunlem1  20826  voliunlem3  20874  uniioombllem2  20904  dyadss  20915  dvlipcn  21307  dv11cn  21314  dvle  21320  dvfsumge  21335  dvfsumlem2  21340  dvfsumlem4  21342  dvfsum2  21347  dgrsub  21623  vieta1lem2  21661  itgulm2  21758  radcnvlem1  21762  abelthlem7  21787  efcvx  21798  logdivlti  21953  logcnlem4  21974  logccv  21992  cxple2a  22028  cxpaddlelem  22073  cxpaddle  22074  leibpi  22221  scvxcvx  22263  amgmlem  22267  logdiflbnd  22272  ftalem2  22295  ppip1le  22383  ppieq0  22398  ppiltx  22399  chpeq0  22431  chtublem  22434  chtub  22435  logexprlim  22448  perfectlem2  22453  bposlem9  22515  2sqlem8  22595  chebbnd1lem1  22602  vmadivsum  22615  rplogsumlem1  22617  dchrisum0re  22646  dchrisum0lem1  22649  selberglem2  22679  chpdifbndlem1  22686  selberg3lem1  22690  pntrlog2bndlem2  22711  pntrlog2bndlem3  22712  pntrlog2bndlem6  22716  pntpbnd2  22720  pntibndlem2  22724  pntlemb  22730  pntlemr  22735  pntlemo  22740  ostth2lem2  22767  ostth2lem3  22768  occllem  24528  nmcexi  25252  cnlnadjlem7  25299  hmopidmchi  25377  omndadd2d  25994  omndmul2  25998  omndmul3  25999  ogrpinvOLD  26001  ogrpinv0le  26002  ogrpaddltrbid  26007  ogrpinv0lt  26009  isarchi3  26027  archirngz  26029  archiabllem1b  26032  gsumle  26097  orngsqr  26124  ornglmulle  26125  orngrmulle  26126  isarchiofld  26137  eulerpartlemgc  26592  dstfrvclim1  26707  lgamgulmlem2  26863  lgamgulmlem5  26866  lgambdd  26870  lgamcvg2  26888  subfaclim  26923  ovoliunnfl  28274  itg2addnclem3  28286  ftc1anclem8  28315  cntotbnd  28536  rrnmet  28569  jm2.24nn  29144  jm2.27a  29196  idomrootle  29402  stoweidlem10  29648  stoweidlem11  29649  stoweidlem13  29651  stoweidlem14  29652  stoweidlem28  29666  stirlinglem11  29722  stirlinglem12  29723  3atlem1  32697  3atlem2  32698  llncvrlpln2  32771  lplncvrlvol2  32829  dalem25  32912  dalawlem7  33091  dalawlem11  33095  cdleme22g  33562  cdlemg18b  33893  cdlemg46  33949  dia2dimlem3  34281  dihord2  34442