Theorem 3brtr3d 4684

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

Syntax hints:   -> wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  ofrval  6907  difsnen  8042  domunsncan  8060  phplem2  8140  infdifsn  8554  ltaddnq  9796  lemul2a  10878  mul2lt0rlt0  11932  xleadd2a  12084  xlemul2a  12119  monoord2  12832  expubnd  12921  bernneq2  12991  hashfun  13224  sqrlem2  13984  abs2dif2  14073  rlimdiv  14376  isercolllem1  14395  iseraltlem2  14413  iseraltlem3  14414  fsum00  14530  seqabs  14546  cvgcmp  14548  mertenslem1  14616  eftlub  14839  eirrlem  14932  bitscmp  15160  prmreclem1  15620  invisoinvl  16450  efgcpbl2  18170  pgpfaclem2  18481  unitgrp  18667  xblss2  22207  xmstri2  22271  mstri2  22272  xmstri  22273  mstri  22274  xmstri3  22275  mstri3  22276  msrtri  22277  nrmmetd  22379  nmtri  22430  nmoi2  22534  xrsxmet  22612  xrge0gsumle  22636  iccpnfhmeo  22744  pcorev2  22828  pi1cpbl  22844  rrxmet  23191  ovoliunlem1  23270  voliunlem3  23320  uniioombllem2  23351  dyadss  23362  dvlipcn  23757  dv11cn  23764  dvle  23770  dvfsumge  23785  dvfsumlem2  23790  dvfsumlem4  23792  dvfsum2  23797  dgrsub  24028  vieta1lem2  24066  itgulm2  24163  radcnvlem1  24167  abelthlem7  24192  efcvx  24203  logdivlti  24366  logcnlem4  24391  logccv  24409  cxple2a  24445  cxpaddlelem  24492  cxpaddle  24493  leibpi  24669  scvxcvx  24712  amgmlem  24716  logdiflbnd  24721  lgamgulmlem2  24756  lgamgulmlem5  24759  lgambdd  24763  lgamcvg2  24781  ftalem2  24800  ppip1le  24887  ppieq0  24902  ppiltx  24903  chpeq0  24933  chtublem  24936  chtub  24937  logexprlim  24950  perfectlem2  24955  bposlem9  25017  2sqlem8  25151  chebbnd1lem1  25158  vmadivsum  25171  rplogsumlem1  25173  dchrisum0re  25202  dchrisum0lem1  25205  selberglem2  25235  chpdifbndlem1  25242  selberg3lem1  25246  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem6  25272  pntpbnd2  25276  pntibndlem2  25280  pntlemb  25286  pntlemr  25291  pntlemo  25296  ostth2lem2  25323  ostth2lem3  25324  tgcgrsub2  25490  legso  25494  krippenlem  25585  midex  25629  opphllem3  25641  trgcopy  25696  occllem  28162  nmcexi  28885  cnlnadjlem7  28932  hmopidmchi  29010  omndadd2d  29708  omndmul2  29712  omndmul3  29713  ogrpinvOLD  29715  ogrpinv0le  29716  ogrpaddltbi  29719  ogrpaddltrbid  29721  ogrpinv0lt  29723  isarchi3  29741  archirngz  29743  archiabllem1b  29746  gsumle  29779  orngsqr  29804  ornglmulle  29805  orngrmulle  29806  isarchiofld  29817  esum2d  30155  omssubadd  30362  carsgclctun  30383  eulerpartlemgc  30424  dstfrvclim1  30539  fdvneggt  30678  fdvnegge  30680  logdivsqrle  30728  hgt750lemb  30734  subfaclim  31170  nosupbnd2lem1  31861  ovoliunnfl  33451  itg2addnclem3  33463  ftc1anclem8  33492  cntotbnd  33595  rrnmet  33628  3atlem1  34769  3atlem2  34770  llncvrlpln2  34843  lplncvrlvol2  34901  dalem25  34984  dalawlem7  35163  dalawlem11  35167  cdleme22g  35636  cdlemg18b  35967  cdlemg46  36023  dia2dimlem3  36355  dihord2  36516  jm2.24nn  37526  jm2.27a  37572  idomrootle  37773  amgm2d  38501  amgm3d  38502  amgm4d  38503  binomcxplemrat  38549  binomcxplemnotnn0  38555  ioossioobi  39743  ioodvbdlimc2lem  40149  stoweidlem10  40227  stoweidlem11  40228  stoweidlem13  40230  stoweidlem14  40231  stoweidlem28  40245  stirlinglem11  40301  stirlinglem12  40302  dirkercncflem4  40323  fourierdlem4  40328  fourierdlem6  40330  fourierdlem11  40335  fourierdlem42  40366  fourierdlem51  40374  fourierdlem73  40396  fourierdlem79  40402  2pwp1prm  41503  perfectALTVlem2  41631  fllogbd  42354  nnpw2blen  42374  amgmwlem  42548  amgmlemALT  42549  amgmw2d  42550  young2d  42551