Theorem 3brtr3d 4466

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

Syntax hints:   -> wi 4   = wceq 1383   class class class wbr 4437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438

This theorem is referenced by:  ofrval  6535  difsnen  7601  domunsncan  7619  phplem2  7699  infdifsn  8076  ltaddnq  9355  lemul2a  10404  xleadd2a  11456  xlemul2a  11491  monoord2  12119  expubnd  12207  bernneq2  12274  hashfun  12476  sqrlem2  13058  abs2dif2  13147  rlimdiv  13449  isercolllem1  13468  iseraltlem2  13486  iseraltlem3  13487  fsum00  13593  seqabs  13609  cvgcmp  13611  mertenslem1  13674  eftlub  13825  eirrlem  13918  bitscmp  14069  prmreclem1  14415  efgcpbl2  16753  pgpfaclem2  17111  unitgrp  17294  xblss2  20882  xmstri2  20946  mstri2  20947  xmstri  20948  mstri  20949  xmstri3  20950  mstri3  20951  msrtri  20952  nrmmetd  21072  nmtri  21122  nmoi2  21214  xrsxmet  21291  xrge0gsumle  21315  iccpnfhmeo  21422  pcorev2  21505  pi1cpbl  21521  rrxmet  21812  ovoliunlem1  21890  voliunlem3  21939  uniioombllem2  21969  dyadss  21980  dvlipcn  22372  dv11cn  22379  dvle  22385  dvfsumge  22400  dvfsumlem2  22405  dvfsumlem4  22407  dvfsum2  22412  dgrsub  22645  vieta1lem2  22683  itgulm2  22780  radcnvlem1  22784  abelthlem7  22809  efcvx  22820  logdivlti  22981  logcnlem4  23002  logccv  23020  cxple2a  23056  cxpaddlelem  23101  cxpaddle  23102  leibpi  23249  scvxcvx  23291  amgmlem  23295  logdiflbnd  23300  ftalem2  23323  ppip1le  23411  ppieq0  23426  ppiltx  23427  chpeq0  23459  chtublem  23462  chtub  23463  logexprlim  23476  perfectlem2  23481  bposlem9  23543  2sqlem8  23623  chebbnd1lem1  23630  vmadivsum  23643  rplogsumlem1  23645  dchrisum0re  23674  dchrisum0lem1  23677  selberglem2  23707  chpdifbndlem1  23714  selberg3lem1  23718  pntrlog2bndlem2  23739  pntrlog2bndlem3  23740  pntrlog2bndlem6  23744  pntpbnd2  23748  pntibndlem2  23752  pntlemb  23758  pntlemr  23763  pntlemo  23768  ostth2lem2  23795  ostth2lem3  23796  legso  23961  krippenlem  24043  midex  24087  opphllem3  24097  occllem  26197  nmcexi  26921  cnlnadjlem7  26968  hmopidmchi  27046  mul2lt0rlt0  27541  omndadd2d  27675  omndmul2  27679  omndmul3  27680  ogrpinvOLD  27682  ogrpinv0le  27683  ogrpaddltbi  27686  ogrpaddltrbid  27688  ogrpinv0lt  27690  isarchi3  27708  archirngz  27710  archiabllem1b  27713  gsumle  27747  orngsqr  27771  ornglmulle  27772  orngrmulle  27773  isarchiofld  27784  eulerpartlemgc  28278  dstfrvclim1  28393  lgamgulmlem2  28549  lgamgulmlem5  28552  lgambdd  28556  lgamcvg2  28574  subfaclim  28609  ovoliunnfl  30031  itg2addnclem3  30043  ftc1anclem8  30072  cntotbnd  30267  rrnmet  30300  jm2.24nn  30872  jm2.27a  30922  idomrootle  31128  ioossioobi  31493  ioodvbdlimc2lem  31635  stoweidlem10  31681  stoweidlem11  31682  stoweidlem13  31684  stoweidlem14  31685  stoweidlem28  31699  stirlinglem11  31755  stirlinglem12  31756  dirkercncflem4  31777  fourierdlem4  31782  fourierdlem6  31784  fourierdlem11  31789  fourierdlem42  31820  fourierdlem51  31829  fourierdlem73  31851  fourierdlem79  31857  3atlem1  34947  3atlem2  34948  llncvrlpln2  35021  lplncvrlvol2  35079  dalem25  35162  dalawlem7  35341  dalawlem11  35345  cdleme22g  35814  cdlemg18b  36145  cdlemg46  36201  dia2dimlem3  36533  dihord2  36694