Theorem 3brtr3d 5155

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  ofrval  7688  difsnen  9072  domunsncan  9091  phplem2OLD  9234  infdifsn  9676  ltaddnq  10993  lemul2a  12101  mul2lt0rlt0  13116  xleadd2a  13275  xlemul2a  13310  monoord2  14056  expubnd  14201  bernneq2  14253  hashfun  14460  01sqrexlem2  15267  abs2dif2  15357  rlimdiv  15667  isercolllem1  15686  iseraltlem2  15704  iseraltlem3  15705  fsum00  15819  seqabs  15835  cvgcmp  15837  mertenslem1  15905  fprodle  16017  eftlub  16132  eirrlem  16227  bitscmp  16462  prmreclem1  16941  invisoinvl  17808  efgcpbl2  19743  pgpfaclem2  20070  unitgrp  20348  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  25365  ovoliunlem1  25460  voliunlem3  25510  uniioombllem2  25541  dyadss  25552  dvlipcn  25956  dv11cn  25963  dvle  25969  dvfsumge  25985  dvfsumlem2  25990  dvfsumlem2OLD  25991  dvfsumlem4  25993  dvfsum2  25998  idomrootle  26135  dgrsub  26235  vieta1lem2  26276  itgulm2  26375  radcnvlem1  26379  abelthlem7  26405  efcvx  26416  logdivlti  26586  logcnlem4  26611  logccv  26629  cxple2a  26665  cxpaddlelem  26718  cxpaddle  26719  leibpi  26909  scvxcvx  26953  amgmlem  26957  logdiflbnd  26962  lgamgulmlem2  26997  lgamgulmlem5  27000  lgambdd  27004  lgamcvg2  27022  ftalem2  27041  ppip1le  27128  ppieq0  27143  ppiltx  27144  chpeq0  27176  chtublem  27179  chtub  27180  logexprlim  27193  perfectlem2  27198  bposlem9  27260  2sqlem8  27394  chebbnd1lem1  27437  vmadivsum  27450  rplogsumlem1  27452  dchrisum0re  27481  dchrisum0lem1  27484  selberglem2  27514  chpdifbndlem1  27521  selberg3lem1  27525  pntrlog2bndlem2  27546  pntrlog2bndlem3  27547  pntrlog2bndlem6  27551  pntpbnd2  27555  pntibndlem2  27559  pntlemb  27565  pntlemr  27570  pntlemo  27575  ostth2lem2  27602  ostth2lem3  27603  nosupbnd2lem1  27684  noinfbnd2lem1  27699  mulsgt0  28104  tgcgrsub2  28579  legso  28583  krippenlem  28674  midex  28721  opphllem3  28733  trgcopy  28788  occllem  31289  nmcexi  32012  cnlnadjlem7  32059  hmopidmchi  32137  oexpled  32831  mgcf1o  32988  chnind  32996  chnlt  32998  chnso  32999  omndadd2d  33081  omndmul2  33085  omndmul3  33086  ogrpinv0le  33088  ogrpaddltbi  33091  ogrpaddltrbid  33093  ogrpinv0lt  33095  gsumle  33097  isarchi3  33190  archirngz  33192  archiabllem1b  33195  orngsqr  33331  ornglmulle  33332  orngrmulle  33333  isarchiofld  33344  cos9thpiminplylem1  33821  esum2d  34129  omssubadd  34337  carsgclctun  34358  eulerpartlemgc  34399  dstfrvclim1  34515  fdvneggt  34637  fdvnegge  34639  logdivsqrle  34687  hgt750lemb  34693  subfaclim  35215  ovoliunnfl  37691  itg2addnclem3  37702  ftc1anclem8  37729  cntotbnd  37825  rrnmet  37858  3atlem1  39507  3atlem2  39508  llncvrlpln2  39581  lplncvrlvol2  39639  dalem25  39722  dalawlem7  39901  dalawlem11  39905  cdleme22g  40372  cdlemg18b  40703  cdlemg46  40759  dia2dimlem3  41090  dihord2  41251  3lexlogpow5ineq2  42073  3lexlogpow2ineq1  42076  3lexlogpow5ineq5  42078  aks4d1p1p7  42092  aks4d1p1  42094  aks4d1p6  42099  aks6d1c2lem4  42145  sticksstones6  42169  bcled  42196  bcle2d  42197  aks6d1c7lem1  42198  jm2.24nn  42958  jm2.27a  43004  amgm2d  44197  amgm3d  44198  amgm4d  44199  binomcxplemrat  44349  binomcxplemnotnn0  44355  monoord2xrv  45490  ioossioobi  45526  ioodvbdlimc2lem  45943  stoweidlem10  46019  stoweidlem11  46020  stoweidlem13  46022  stoweidlem14  46023  stoweidlem28  46037  stirlinglem11  46093  stirlinglem12  46094  dirkercncflem4  46115  fourierdlem4  46120  fourierdlem6  46122  fourierdlem11  46127  fourierdlem42  46158  fourierdlem51  46166  fourierdlem73  46188  fourierdlem79  46194  2pwp1prm  47583  perfectALTVlem2  47716  fllogbd  48520  nnpw2blen  48540  funcoppc4  49067  amgmwlem  49646  amgmlemALT  49647  amgmw2d  49648  young2d  49649