Theorem 3brtr3d 4450

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

Syntax hints:   -> wi 4   = wceq 1437   class class class wbr 4420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421

This theorem is referenced by:  ofrval  6551  difsnen  7656  domunsncan  7674  phplem2  7754  infdifsn  8163  ltaddnq  9399  lemul2a  10460  mul2lt0rlt0  11398  xleadd2a  11540  xlemul2a  11575  monoord2  12243  expubnd  12332  bernneq2  12398  hashfun  12606  sqrlem2  13295  abs2dif2  13384  rlimdiv  13696  isercolllem1  13715  iseraltlem2  13736  iseraltlem3  13737  fsum00  13845  seqabs  13861  cvgcmp  13863  mertenslem1  13927  eftlub  14150  eirrlem  14243  bitscmp  14399  prmreclem1  14847  invisoinvl  15682  efgcpbl2  17394  pgpfaclem2  17702  unitgrp  17882  xblss2  21403  xmstri2  21467  mstri2  21468  xmstri  21469  mstri  21470  xmstri3  21471  mstri3  21472  msrtri  21473  nrmmetd  21575  nmtri  21625  nmoi2  21721  nmoi2OLD  21737  xrsxmet  21813  xrge0gsumle  21837  iccpnfhmeo  21959  pcorev2  22045  pi1cpbl  22061  rrxmet  22348  ovoliunlem1  22441  voliunlem3  22491  uniioombllem2  22526  uniioombllem2OLD  22527  dyadss  22538  dvlipcn  22932  dv11cn  22939  dvle  22945  dvfsumge  22960  dvfsumlem2  22965  dvfsumlem4  22967  dvfsum2  22972  dgrsub  23212  vieta1lem2  23250  itgulm2  23350  radcnvlem1  23354  abelthlem7  23379  efcvx  23390  logdivlti  23555  logcnlem4  23576  logccv  23594  cxple2a  23630  cxpaddlelem  23677  cxpaddle  23678  leibpi  23854  scvxcvx  23897  amgmlem  23901  logdiflbnd  23906  lgamgulmlem2  23941  lgamgulmlem5  23944  lgambdd  23948  lgamcvg2  23966  ftalem2  23984  ppip1le  24074  ppieq0  24089  ppiltx  24090  chpeq0  24122  chtublem  24125  chtub  24126  logexprlim  24139  perfectlem2  24144  bposlem9  24206  2sqlem8  24286  chebbnd1lem1  24293  vmadivsum  24306  rplogsumlem1  24308  dchrisum0re  24337  dchrisum0lem1  24340  selberglem2  24370  chpdifbndlem1  24377  selberg3lem1  24381  pntrlog2bndlem2  24402  pntrlog2bndlem3  24403  pntrlog2bndlem6  24407  pntpbnd2  24411  pntibndlem2  24415  pntlemb  24421  pntlemr  24426  pntlemo  24431  ostth2lem2  24458  ostth2lem3  24459  tgcgrsub2  24626  legso  24630  krippenlem  24721  midex  24765  opphllem3  24777  trgcopy  24832  occllem  26941  nmcexi  27664  cnlnadjlem7  27711  hmopidmchi  27789  omndadd2d  28465  omndmul2  28469  omndmul3  28470  ogrpinvOLD  28472  ogrpinv0le  28473  ogrpaddltbi  28476  ogrpaddltrbid  28478  ogrpinv0lt  28480  isarchi3  28498  archirngz  28500  archiabllem1b  28503  gsumle  28536  orngsqr  28562  ornglmulle  28563  orngrmulle  28564  isarchiofld  28575  esum2d  28909  omssubadd  29123  omssubaddOLD  29127  carsgclctun  29148  eulerpartlemgc  29190  dstfrvclim1  29305  subfaclim  29906  ovoliunnfl  31895  itg2addnclem3  31908  ftc1anclem8  31937  cntotbnd  32041  rrnmet  32074  3atlem1  32966  3atlem2  32967  llncvrlpln2  33040  lplncvrlvol2  33098  dalem25  33181  dalawlem7  33360  dalawlem11  33364  cdleme22g  33833  cdlemg18b  34164  cdlemg46  34220  dia2dimlem3  34552  dihord2  34713  jm2.24nn  35728  jm2.27a  35779  idomrootle  35988  amgm2d  36507  amgm3d  36508  amgm4d  36509  binomcxplemrat  36556  binomcxplemnotnn0  36562  ioossioobi  37448  ioodvbdlimc2lem  37627  ioodvbdlimc2lemOLD  37628  stoweidlem10  37689  stoweidlem11  37690  stoweidlem13  37692  stoweidlem14  37693  stoweidlem28  37707  stirlinglem11  37765  stirlinglem12  37766  dirkercncflem4  37787  fourierdlem4  37792  fourierdlem6  37794  fourierdlem11  37799  fourierdlem42  37831  fourierdlem42OLD  37832  fourierdlem51  37840  fourierdlem73  37862  fourierdlem79  37868  perfectALTVlem2  38555  fllogbd  39644  nnpw2blen  39664