Theorem 3brtr3d 4468

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

Syntax hints:   -> wi 4   = wceq 1398   class class class wbr 4439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440

This theorem is referenced by:  ofrval  6523  difsnen  7592  domunsncan  7610  phplem2  7690  infdifsn  8064  ltaddnq  9341  lemul2a  10393  xleadd2a  11449  xlemul2a  11484  monoord2  12123  expubnd  12211  bernneq2  12278  hashfun  12482  sqrlem2  13162  abs2dif2  13251  rlimdiv  13553  isercolllem1  13572  iseraltlem2  13590  iseraltlem3  13591  fsum00  13697  seqabs  13713  cvgcmp  13715  mertenslem1  13778  eftlub  13929  eirrlem  14022  bitscmp  14175  prmreclem1  14521  invisoinvl  15281  efgcpbl2  16977  pgpfaclem2  17331  unitgrp  17514  xblss2  21074  xmstri2  21138  mstri2  21139  xmstri  21140  mstri  21141  xmstri3  21142  mstri3  21143  msrtri  21144  nrmmetd  21264  nmtri  21314  nmoi2  21406  xrsxmet  21483  xrge0gsumle  21507  iccpnfhmeo  21614  pcorev2  21697  pi1cpbl  21713  rrxmet  22004  ovoliunlem1  22082  voliunlem3  22131  uniioombllem2  22161  dyadss  22172  dvlipcn  22564  dv11cn  22571  dvle  22577  dvfsumge  22592  dvfsumlem2  22597  dvfsumlem4  22599  dvfsum2  22604  dgrsub  22838  vieta1lem2  22876  itgulm2  22973  radcnvlem1  22977  abelthlem7  23002  efcvx  23013  logdivlti  23176  logcnlem4  23197  logccv  23215  cxple2a  23251  cxpaddlelem  23296  cxpaddle  23297  leibpi  23473  scvxcvx  23516  amgmlem  23520  logdiflbnd  23525  ftalem2  23548  ppip1le  23636  ppieq0  23651  ppiltx  23652  chpeq0  23684  chtublem  23687  chtub  23688  logexprlim  23701  perfectlem2  23706  bposlem9  23768  2sqlem8  23848  chebbnd1lem1  23855  vmadivsum  23868  rplogsumlem1  23870  dchrisum0re  23899  dchrisum0lem1  23902  selberglem2  23932  chpdifbndlem1  23939  selberg3lem1  23943  pntrlog2bndlem2  23964  pntrlog2bndlem3  23965  pntrlog2bndlem6  23969  pntpbnd2  23973  pntibndlem2  23977  pntlemb  23983  pntlemr  23988  pntlemo  23993  ostth2lem2  24020  ostth2lem3  24021  legso  24189  krippenlem  24271  midex  24315  opphllem3  24325  occllem  26422  nmcexi  27146  cnlnadjlem7  27193  hmopidmchi  27271  mul2lt0rlt0  27799  omndadd2d  27935  omndmul2  27939  omndmul3  27940  ogrpinvOLD  27942  ogrpinv0le  27943  ogrpaddltbi  27946  ogrpaddltrbid  27948  ogrpinv0lt  27950  isarchi3  27968  archirngz  27970  archiabllem1b  27973  gsumle  28007  orngsqr  28032  ornglmulle  28033  orngrmulle  28034  isarchiofld  28045  esum2d  28325  omssubadd  28511  carsgclctun  28532  eulerpartlemgc  28568  dstfrvclim1  28683  lgamgulmlem2  28839  lgamgulmlem5  28842  lgambdd  28846  lgamcvg2  28864  subfaclim  28899  ovoliunnfl  30299  itg2addnclem3  30311  ftc1anclem8  30340  cntotbnd  30535  rrnmet  30568  jm2.24nn  31139  jm2.27a  31189  idomrootle  31396  binomcxplemrat  31499  binomcxplemnotnn0  31505  ioossioobi  31799  ioodvbdlimc2lem  31973  stoweidlem10  32034  stoweidlem11  32035  stoweidlem13  32037  stoweidlem14  32038  stoweidlem28  32052  stirlinglem11  32108  stirlinglem12  32109  dirkercncflem4  32130  fourierdlem4  32135  fourierdlem6  32137  fourierdlem11  32142  fourierdlem42  32173  fourierdlem51  32182  fourierdlem73  32204  fourierdlem79  32210  perfectALTVlem2  32616  fllogbd  33454  nnpw2blen  33474  3atlem1  35623  3atlem2  35624  llncvrlpln2  35697  lplncvrlvol2  35755  dalem25  35838  dalawlem7  36017  dalawlem11  36021  cdleme22g  36490  cdlemg18b  36821  cdlemg46  36877  dia2dimlem3  37209  dihord2  37370