Theorem 3brtr3d 5116

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  ofrval  7643  difsnen  8997  domunsncan  9015  infdifsn  9578  ltaddnq  10897  lemul2a  12010  mul2lt0rlt0  13046  xleadd2a  13206  xlemul2a  13241  monoord2  13995  expubnd  14140  bernneq2  14192  hashfun  14399  01sqrexlem2  15205  abs2dif2  15296  rlimdiv  15608  isercolllem1  15627  iseraltlem2  15645  iseraltlem3  15646  fsum00  15761  seqabs  15777  cvgcmp  15779  mertenslem1  15849  fprodle  15961  eftlub  16076  eirrlem  16171  bitscmp  16407  prmreclem1  16887  invisoinvl  17757  chnind  18587  chnlt  18589  chnso  18590  ex-chn1  18603  efgcpbl2  19732  pgpfaclem2  20059  omndadd2d  20105  omndmul2  20108  omndmul3  20109  ogrpinv0le  20111  ogrpaddltbi  20114  ogrpaddltrbid  20116  ogrpinv0lt  20118  gsumle  20120  unitgrp  20363  orngsqr  20843  ornglmulle  20844  orngrmulle  20845  xblss2  24367  xmstri2  24431  mstri2  24432  xmstri  24433  mstri  24434  xmstri3  24435  mstri3  24436  msrtri  24437  nrmmetd  24539  nmtri  24591  nmoi2  24695  xrsxmet  24775  xrge0gsumle  24799  iccpnfhmeo  24912  pcorev2  24995  pi1cpbl  25011  rrxmet  25375  ovoliunlem1  25469  voliunlem3  25519  uniioombllem2  25550  dyadss  25561  dvlipcn  25961  dv11cn  25968  dvle  25974  dvfsumge  25989  dvfsumlem2  25994  dvfsumlem4  25996  dvfsum2  26001  idomrootle  26138  dgrsub  26237  vieta1lem2  26277  itgulm2  26374  radcnvlem1  26378  abelthlem7  26403  efcvx  26414  logdivlti  26584  logcnlem4  26609  logccv  26627  cxple2a  26663  cxpaddlelem  26715  cxpaddle  26716  leibpi  26906  scvxcvx  26949  amgmlem  26953  logdiflbnd  26958  lgamgulmlem2  26993  lgamgulmlem5  26996  lgambdd  27000  lgamcvg2  27018  ftalem2  27037  ppip1le  27124  ppieq0  27139  ppiltx  27140  chpeq0  27171  chtublem  27174  chtub  27175  logexprlim  27188  perfectlem2  27193  bposlem9  27255  2sqlem8  27389  chebbnd1lem1  27432  vmadivsum  27445  rplogsumlem1  27447  dchrisum0re  27476  dchrisum0lem1  27479  selberglem2  27509  chpdifbndlem1  27516  selberg3lem1  27520  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem6  27546  pntpbnd2  27550  pntibndlem2  27554  pntlemb  27560  pntlemr  27565  pntlemo  27570  ostth2lem2  27597  ostth2lem3  27598  nosupbnd2lem1  27679  noinfbnd2lem1  27694  mulsgt0  28136  bdayfinbndlem1  28459  tgcgrsub2  28663  legso  28667  krippenlem  28758  midex  28805  opphllem3  28817  trgcopy  28872  occllem  31374  nmcexi  32097  cnlnadjlem7  32144  hmopidmchi  32222  oexpled  32920  mgcf1o  33063  isarchi3  33248  archirngz  33250  archiabllem1b  33253  isarchiofld  33260  cos9thpiminplylem1  33926  esum2d  34237  omssubadd  34444  carsgclctun  34465  eulerpartlemgc  34506  dstfrvclim1  34622  fdvneggt  34744  fdvnegge  34746  logdivsqrle  34794  hgt750lemb  34800  subfaclim  35370  ovoliunnfl  37983  itg2addnclem3  37994  ftc1anclem8  38021  cntotbnd  38117  rrnmet  38150  3atlem1  39929  3atlem2  39930  llncvrlpln2  40003  lplncvrlvol2  40061  dalem25  40144  dalawlem7  40323  dalawlem11  40327  cdleme22g  40794  cdlemg18b  41125  cdlemg46  41181  dia2dimlem3  41512  dihord2  41673  3lexlogpow5ineq2  42494  3lexlogpow2ineq1  42497  3lexlogpow5ineq5  42499  aks4d1p1p7  42513  aks4d1p1  42515  aks4d1p6  42520  aks6d1c2lem4  42566  sticksstones6  42590  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  jm2.24nn  43387  jm2.27a  43433  amgm2d  44625  amgm3d  44626  amgm4d  44627  binomcxplemrat  44777  binomcxplemnotnn0  44783  monoord2xrv  45911  ioossioobi  45947  ioodvbdlimc2lem  46362  stoweidlem10  46438  stoweidlem11  46439  stoweidlem13  46441  stoweidlem14  46442  stoweidlem28  46456  stirlinglem11  46512  stirlinglem12  46513  dirkercncflem4  46534  fourierdlem4  46539  fourierdlem6  46541  fourierdlem11  46546  fourierdlem42  46577  fourierdlem51  46585  fourierdlem73  46607  fourierdlem79  46613  chnerlem2  47313  2pwp1prm  48052  perfectALTVlem2  48198  fllogbd  49036  nnpw2blen  49056  funcoppc4  49619  amgmwlem  50277  amgmlemALT  50278  amgmw2d  50279  young2d  50280