Theorem 3brtr3d 5136

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 18-Oct-1999.)

Hypotheses

Ref	Expression
3brtr3d.1	⊢ (𝜑 → 𝐴𝑅𝐵)
3brtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3brtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3brtr3d	⊢ (𝜑 → 𝐶𝑅𝐷)

Proof of Theorem 3brtr3d

Step	Hyp	Ref	Expression
1		3brtr3d.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		3brtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3		3brtr3d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	breq12d 5118	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷))
5	1, 4	mpbid 235	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

Syntax hints:   → wi 4   = wceq 1563   class class class wbr 5105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106

This theorem is referenced by:  ofrval  7676  difsnen  9035  domunsncan  9053  infdifsn  9614  ltaddnq  10947  lemul2a  12061  mul2lt0rlt0  13111  xleadd2a  13271  xlemul2a  13306  monoord2  14060  expubnd  14205  bernneq2  14257  hashfun  14464  01sqrexlem2  15284  abs2dif2  15375  rlimdiv  15687  isercolllem1  15706  iseraltlem2  15724  iseraltlem3  15725  fsum00  15840  seqabs  15856  cvgcmp  15858  mertenslem1  15928  fprodle  16040  eftlub  16155  eirrlem  16250  bitscmp  16486  prmreclem1  16966  invisoinvl  17837  chnind  18667  chnlt  18669  chnso  18670  ex-chn1  18683  efgcpbl2  19818  pgpfaclem2  20145  omndadd2d  20191  omndmul2  20194  omndmul3  20195  ogrpinv0le  20197  ogrpaddltbi  20200  ogrpaddltrbid  20202  ogrpinv0lt  20204  gsumle  20206  unitgrp  20456  orngsqr  20938  ornglmulle  20939  orngrmulle  20940  xblss2  24520  xmstri2  24584  mstri2  24585  xmstri  24586  mstri  24587  xmstri3  24588  mstri3  24589  msrtri  24590  nrmmetd  24692  nmtri  24744  nmoi2  24848  xrsxmet  24928  xrge0gsumle  24952  iccpnfhmeo  25065  pcorev2  25148  pi1cpbl  25164  rrxmet  25528  ovoliunlem1  25622  voliunlem3  25672  uniioombllem2  25703  dyadss  25714  dvlipcn  26114  dv11cn  26121  dvle  26127  dvfsumge  26142  dvfsumlem2  26147  dvfsumlem4  26149  dvfsum2  26154  idomrootle  26291  dgrsub  26390  vieta1lem2  26433  itgulm2  26530  radcnvlem1  26534  abelthlem7  26559  efcvx  26570  logdivlti  26743  logcnlem4  26768  logccv  26786  cxple2a  26822  cxpaddlelem  26874  cxpaddle  26875  leibpi  27065  scvxcvx  27108  amgmlem  27112  logdiflbnd  27117  lgamgulmlem2  27152  lgamgulmlem5  27155  lgambdd  27159  lgamcvg2  27177  ftalem2  27196  ppip1le  27283  ppieq0  27298  ppiltx  27299  chpeq0  27330  chtublem  27333  chtub  27334  logexprlim  27347  perfectlem2  27352  bposlem9  27414  2sqlem8  27548  chebbnd1lem1  27591  vmadivsum  27604  rplogsumlem1  27606  dchrisum0re  27635  dchrisum0lem1  27638  selberglem2  27668  chpdifbndlem1  27675  selberg3lem1  27679  pntrlog2bndlem2  27700  pntrlog2bndlem3  27701  pntrlog2bndlem6  27705  pntpbnd2  27709  pntibndlem2  27713  pntlemb  27719  pntlemr  27724  pntlemo  27729  ostth2lem2  27756  ostth2lem3  27757  nosupbnd2lem1  27837  noinfbnd2lem1  27852  mulsgt0  28295  bdayfinbndlem1  28618  tgcgrsub2  28822  legso  28826  krippenlem  28921  midex  28968  opphllem3  28980  trgcopy  29056  occllem  31564  nmcexi  32287  cnlnadjlem7  32334  hmopidmchi  32412  oexpled  33093  mgcf1o  33236  isarchi3  33420  archirngz  33422  archiabllem1b  33425  isarchiofld  33432  cos9thpiminplylem1  34089  esum2d  34400  omssubadd  34607  carsgclctun  34628  eulerpartlemgc  34669  dstfrvclim1  34785  fdvneggt  34904  fdvnegge  34906  logdivsqrle  34954  hgt750lemb  34960  subfaclim  35551  ovoliunnfl  38173  itg2addnclem3  38184  ftc1anclem8  38211  cntotbnd  38307  rrnmet  38340  3atlem1  40119  3atlem2  40120  llncvrlpln2  40193  lplncvrlvol2  40251  dalem25  40334  dalawlem7  40513  dalawlem11  40517  cdleme22g  40984  cdlemg18b  41315  cdlemg46  41371  dia2dimlem3  41702  dihord2  41863  3lexlogpow5ineq2  42684  3lexlogpow2ineq1  42687  3lexlogpow5ineq5  42689  aks4d1p1p7  42703  aks4d1p1  42705  aks4d1p6  42710  aks6d1c2lem4  42756  sticksstones6  42780  bcled  42807  bcle2d  42808  aks6d1c7lem1  42809  jm2.24nn  43548  jm2.27a  43594  amgm2d  44786  amgm3d  44787  amgm4d  44788  binomcxplemrat  44924  binomcxplemnotnn0  44930  monoord2xrv  46055  ioossioobi  46091  ioodvbdlimc2lem  46506  stoweidlem10  46582  stoweidlem11  46583  stoweidlem13  46585  stoweidlem14  46586  stoweidlem28  46600  stirlinglem11  46656  stirlinglem12  46657  dirkercncflem4  46678  fourierdlem4  46683  fourierdlem6  46685  fourierdlem11  46690  fourierdlem42  46721  fourierdlem51  46729  fourierdlem73  46751  fourierdlem79  46757  chnerlem2  47457  2pwp1prm  48196  perfectALTVlem2  48342  fllogbd  49191  nnpw2blen  49211  funcoppc4  49773  amgmwlem  50431  amgmlemALT  50432  amgmw2d  50433  young2d  50434