Theorem 3brtr3d 4446

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

Syntax hints:   -> wi 4   = wceq 1455   class class class wbr 4416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417

This theorem is referenced by:  ofrval  6568  difsnen  7680  domunsncan  7698  phplem2  7778  infdifsn  8188  ltaddnq  9425  lemul2a  10488  mul2lt0rlt0  11427  xleadd2a  11569  xlemul2a  11604  monoord2  12276  expubnd  12365  bernneq2  12431  hashfun  12642  sqrlem2  13356  abs2dif2  13445  rlimdiv  13758  isercolllem1  13777  iseraltlem2  13798  iseraltlem3  13799  fsum00  13907  seqabs  13923  cvgcmp  13925  mertenslem1  13989  eftlub  14212  eirrlem  14305  bitscmp  14461  prmreclem1  14909  invisoinvl  15744  efgcpbl2  17456  pgpfaclem2  17764  unitgrp  17944  xblss2  21466  xmstri2  21530  mstri2  21531  xmstri  21532  mstri  21533  xmstri3  21534  mstri3  21535  msrtri  21536  nrmmetd  21638  nmtri  21688  nmoi2  21784  nmoi2OLD  21800  xrsxmet  21876  xrge0gsumle  21900  iccpnfhmeo  22022  pcorev2  22108  pi1cpbl  22124  rrxmet  22411  ovoliunlem1  22504  voliunlem3  22554  uniioombllem2  22589  uniioombllem2OLD  22590  dyadss  22601  dvlipcn  22995  dv11cn  23002  dvle  23008  dvfsumge  23023  dvfsumlem2  23028  dvfsumlem4  23030  dvfsum2  23035  dgrsub  23275  vieta1lem2  23313  itgulm2  23413  radcnvlem1  23417  abelthlem7  23442  efcvx  23453  logdivlti  23618  logcnlem4  23639  logccv  23657  cxple2a  23693  cxpaddlelem  23740  cxpaddle  23741  leibpi  23917  scvxcvx  23960  amgmlem  23964  logdiflbnd  23969  lgamgulmlem2  24004  lgamgulmlem5  24007  lgambdd  24011  lgamcvg2  24029  ftalem2  24047  ppip1le  24137  ppieq0  24152  ppiltx  24153  chpeq0  24185  chtublem  24188  chtub  24189  logexprlim  24202  perfectlem2  24207  bposlem9  24269  2sqlem8  24349  chebbnd1lem1  24356  vmadivsum  24369  rplogsumlem1  24371  dchrisum0re  24400  dchrisum0lem1  24403  selberglem2  24433  chpdifbndlem1  24440  selberg3lem1  24444  pntrlog2bndlem2  24465  pntrlog2bndlem3  24466  pntrlog2bndlem6  24470  pntpbnd2  24474  pntibndlem2  24478  pntlemb  24484  pntlemr  24489  pntlemo  24494  ostth2lem2  24521  ostth2lem3  24522  tgcgrsub2  24689  legso  24693  krippenlem  24784  midex  24828  opphllem3  24840  trgcopy  24895  occllem  27005  nmcexi  27728  cnlnadjlem7  27775  hmopidmchi  27853  omndadd2d  28520  omndmul2  28524  omndmul3  28525  ogrpinvOLD  28527  ogrpinv0le  28528  ogrpaddltbi  28531  ogrpaddltrbid  28533  ogrpinv0lt  28535  isarchi3  28553  archirngz  28555  archiabllem1b  28558  gsumle  28591  orngsqr  28616  ornglmulle  28617  orngrmulle  28618  isarchiofld  28629  esum2d  28963  omssubadd  29177  omssubaddOLD  29181  carsgclctun  29202  eulerpartlemgc  29244  dstfrvclim1  29359  subfaclim  29960  ovoliunnfl  32027  itg2addnclem3  32040  ftc1anclem8  32069  cntotbnd  32173  rrnmet  32206  3atlem1  33093  3atlem2  33094  llncvrlpln2  33167  lplncvrlvol2  33225  dalem25  33308  dalawlem7  33487  dalawlem11  33491  cdleme22g  33960  cdlemg18b  34291  cdlemg46  34347  dia2dimlem3  34679  dihord2  34840  jm2.24nn  35854  jm2.27a  35905  idomrootle  36114  amgm2d  36694  amgm3d  36695  amgm4d  36696  binomcxplemrat  36743  binomcxplemnotnn0  36749  ioossioobi  37656  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  stoweidlem10  37908  stoweidlem11  37909  stoweidlem13  37911  stoweidlem14  37912  stoweidlem28  37926  stirlinglem11  37984  stirlinglem12  37985  dirkercncflem4  38006  fourierdlem4  38011  fourierdlem6  38013  fourierdlem11  38018  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem51  38059  fourierdlem73  38081  fourierdlem79  38087  perfectALTVlem2  38882  fllogbd  40644  nnpw2blen  40664