Theorem 3brtr3d 5129

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 5111	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐶𝑅𝐷))
5	1, 4	mpbid 232	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  ofrval  7634  difsnen  8987  domunsncan  9005  infdifsn  9566  ltaddnq  10885  lemul2a  11996  mul2lt0rlt0  13009  xleadd2a  13169  xlemul2a  13204  monoord2  13956  expubnd  14101  bernneq2  14153  hashfun  14360  01sqrexlem2  15166  abs2dif2  15257  rlimdiv  15569  isercolllem1  15588  iseraltlem2  15606  iseraltlem3  15607  fsum00  15721  seqabs  15737  cvgcmp  15739  mertenslem1  15807  fprodle  15919  eftlub  16034  eirrlem  16129  bitscmp  16365  prmreclem1  16844  invisoinvl  17714  chnind  18544  chnlt  18546  chnso  18547  ex-chn1  18560  efgcpbl2  19686  pgpfaclem2  20013  omndadd2d  20059  omndmul2  20062  omndmul3  20063  ogrpinv0le  20065  ogrpaddltbi  20068  ogrpaddltrbid  20070  ogrpinv0lt  20072  gsumle  20074  unitgrp  20319  orngsqr  20799  ornglmulle  20800  orngrmulle  20801  xblss2  24346  xmstri2  24410  mstri2  24411  xmstri  24412  mstri  24413  xmstri3  24414  mstri3  24415  msrtri  24416  nrmmetd  24518  nmtri  24570  nmoi2  24674  xrsxmet  24754  xrge0gsumle  24778  iccpnfhmeo  24899  pcorev2  24984  pi1cpbl  25000  rrxmet  25364  ovoliunlem1  25459  voliunlem3  25509  uniioombllem2  25540  dyadss  25551  dvlipcn  25955  dv11cn  25962  dvle  25968  dvfsumge  25984  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem4  25992  dvfsum2  25997  idomrootle  26134  dgrsub  26234  vieta1lem2  26275  itgulm2  26374  radcnvlem1  26378  abelthlem7  26404  efcvx  26415  logdivlti  26585  logcnlem4  26610  logccv  26628  cxple2a  26664  cxpaddlelem  26717  cxpaddle  26718  leibpi  26908  scvxcvx  26952  amgmlem  26956  logdiflbnd  26961  lgamgulmlem2  26996  lgamgulmlem5  26999  lgambdd  27003  lgamcvg2  27021  ftalem2  27040  ppip1le  27127  ppieq0  27142  ppiltx  27143  chpeq0  27175  chtublem  27178  chtub  27179  logexprlim  27192  perfectlem2  27197  bposlem9  27259  2sqlem8  27393  chebbnd1lem1  27436  vmadivsum  27449  rplogsumlem1  27451  dchrisum0re  27480  dchrisum0lem1  27483  selberglem2  27513  chpdifbndlem1  27520  selberg3lem1  27524  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem6  27550  pntpbnd2  27554  pntibndlem2  27558  pntlemb  27564  pntlemr  27569  pntlemo  27574  ostth2lem2  27601  ostth2lem3  27602  nosupbnd2lem1  27683  noinfbnd2lem1  27698  mulsgt0  28140  bdayfinbndlem1  28463  tgcgrsub2  28667  legso  28671  krippenlem  28762  midex  28809  opphllem3  28821  trgcopy  28876  occllem  31378  nmcexi  32101  cnlnadjlem7  32148  hmopidmchi  32226  oexpled  32928  mgcf1o  33085  isarchi3  33269  archirngz  33271  archiabllem1b  33274  isarchiofld  33281  cos9thpiminplylem1  33939  esum2d  34250  omssubadd  34457  carsgclctun  34478  eulerpartlemgc  34519  dstfrvclim1  34635  fdvneggt  34757  fdvnegge  34759  logdivsqrle  34807  hgt750lemb  34813  subfaclim  35382  ovoliunnfl  37859  itg2addnclem3  37870  ftc1anclem8  37897  cntotbnd  37993  rrnmet  38026  3atlem1  39739  3atlem2  39740  llncvrlpln2  39813  lplncvrlvol2  39871  dalem25  39954  dalawlem7  40133  dalawlem11  40137  cdleme22g  40604  cdlemg18b  40935  cdlemg46  40991  dia2dimlem3  41322  dihord2  41483  3lexlogpow5ineq2  42305  3lexlogpow2ineq1  42308  3lexlogpow5ineq5  42310  aks4d1p1p7  42324  aks4d1p1  42326  aks4d1p6  42331  aks6d1c2lem4  42377  sticksstones6  42401  bcled  42428  bcle2d  42429  aks6d1c7lem1  42430  jm2.24nn  43197  jm2.27a  43243  amgm2d  44435  amgm3d  44436  amgm4d  44437  binomcxplemrat  44587  binomcxplemnotnn0  44593  monoord2xrv  45723  ioossioobi  45759  ioodvbdlimc2lem  46174  stoweidlem10  46250  stoweidlem11  46251  stoweidlem13  46253  stoweidlem14  46254  stoweidlem28  46268  stirlinglem11  46324  stirlinglem12  46325  dirkercncflem4  46346  fourierdlem4  46351  fourierdlem6  46353  fourierdlem11  46358  fourierdlem42  46389  fourierdlem51  46397  fourierdlem73  46419  fourierdlem79  46425  chnerlem2  47123  2pwp1prm  47831  perfectALTVlem2  47964  fllogbd  48802  nnpw2blen  48822  funcoppc4  49385  amgmwlem  50043  amgmlemALT  50044  amgmw2d  50045  young2d  50046