Theorem 3brtr3d 5146

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

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  ofrval  7687  difsnen  9047  domunsncan  9065  infdifsn  9626  ltaddnq  10959  lemul2a  12070  mul2lt0rlt0  13120  xleadd2a  13280  xlemul2a  13315  monoord2  14069  expubnd  14214  bernneq2  14266  hashfun  14474  01sqrexlem2  15294  abs2dif2  15385  rlimdiv  15697  isercolllem1  15716  iseraltlem2  15734  iseraltlem3  15735  fsum00  15850  seqabs  15866  cvgcmp  15868  mertenslem1  15938  fprodle  16050  eftlub  16165  eirrlem  16260  bitscmp  16496  prmreclem1  16976  invisoinvl  17847  chnind  18677  chnlt  18679  chnso  18680  ex-chn1  18693  efgcpbl2  19827  pgpfaclem2  20154  omndadd2d  20200  omndmul2  20203  omndmul3  20204  ogrpinv0le  20206  ogrpaddltbi  20209  ogrpaddltrbid  20211  ogrpinv0lt  20213  gsumle  20215  unitgrp  20465  orngsqr  20947  ornglmulle  20948  orngrmulle  20949  xblss2  24528  xmstri2  24592  mstri2  24593  xmstri  24594  mstri  24595  xmstri3  24596  mstri3  24597  msrtri  24598  nrmmetd  24700  nmtri  24752  nmoi2  24856  xrsxmet  24936  xrge0gsumle  24960  iccpnfhmeo  25073  pcorev2  25156  pi1cpbl  25172  rrxmet  25536  ovoliunlem1  25630  voliunlem3  25680  uniioombllem2  25711  dyadss  25722  dvlipcn  26122  dv11cn  26129  dvle  26135  dvfsumge  26150  dvfsumlem2  26155  dvfsumlem4  26157  dvfsum2  26162  idomrootle  26299  dgrsub  26398  vieta1lem2  26441  itgulm2  26538  radcnvlem1  26542  abelthlem7  26567  efcvx  26578  logdivlti  26751  logcnlem4  26776  logccv  26794  cxple2a  26830  cxpaddlelem  26882  cxpaddle  26883  leibpi  27073  scvxcvx  27116  amgmlem  27120  logdiflbnd  27125  lgamgulmlem2  27160  lgamgulmlem5  27163  lgambdd  27167  lgamcvg2  27185  ftalem2  27204  ppip1le  27291  ppieq0  27306  ppiltx  27307  chpeq0  27338  chtublem  27341  chtub  27342  logexprlim  27355  perfectlem2  27360  bposlem9  27422  2sqlem8  27556  chebbnd1lem1  27599  vmadivsum  27612  rplogsumlem1  27614  dchrisum0re  27643  dchrisum0lem1  27646  selberglem2  27676  chpdifbndlem1  27683  selberg3lem1  27687  pntrlog2bndlem2  27708  pntrlog2bndlem3  27709  pntrlog2bndlem6  27713  pntpbnd2  27717  pntibndlem2  27721  pntlemb  27727  pntlemr  27732  pntlemo  27737  ostth2lem2  27764  ostth2lem3  27765  nosupbnd2lem1  27845  noinfbnd2lem1  27860  mulsgt0  28303  bdayfinbndlem1  28626  tgcgrsub2  28830  legso  28834  krippenlem  28929  midex  28977  opphllem3  28989  trgcopy  29072  perpeqlem  29105  occllem  31596  nmcexi  32319  cnlnadjlem7  32366  hmopidmchi  32444  oexpled  33121  mgcf1o  33264  isarchi3  33448  archirngz  33450  archiabllem1b  33453  isarchiofld  33460  cos9thpiminplylem1  34117  esum2d  34428  omssubadd  34635  carsgclctun  34656  eulerpartlemgc  34697  dstfrvclim1  34813  fdvneggt  34932  fdvnegge  34934  logdivsqrle  34982  hgt750lemb  34988  subfaclim  35579  ovoliunnfl  38201  itg2addnclem3  38212  ftc1anclem8  38239  cntotbnd  38335  rrnmet  38368  3atlem1  40147  3atlem2  40148  llncvrlpln2  40221  lplncvrlvol2  40279  dalem25  40362  dalawlem7  40541  dalawlem11  40545  cdleme22g  41012  cdlemg18b  41343  cdlemg46  41399  dia2dimlem3  41730  dihord2  41891  3lexlogpow5ineq2  42712  3lexlogpow2ineq1  42715  3lexlogpow5ineq5  42717  aks4d1p1p7  42731  aks4d1p1  42733  aks4d1p6  42738  aks6d1c2lem4  42784  sticksstones6  42808  bcled  42835  bcle2d  42836  aks6d1c7lem1  42837  jm2.24nn  43578  jm2.27a  43624  amgm2d  44816  amgm3d  44817  amgm4d  44818  binomcxplemrat  44952  binomcxplemnotnn0  44958  monoord2xrv  46089  ioossioobi  46125  ioodvbdlimc2lem  46540  stoweidlem10  46616  stoweidlem11  46617  stoweidlem13  46619  stoweidlem14  46620  stoweidlem28  46634  stirlinglem11  46690  stirlinglem12  46691  dirkercncflem4  46712  fourierdlem4  46717  fourierdlem6  46719  fourierdlem11  46724  fourierdlem42  46755  fourierdlem51  46763  fourierdlem73  46785  fourierdlem79  46791  chnerlem2  47491  2pwp1prm  48230  perfectALTVlem2  48376  fllogbd  49225  nnpw2blen  49245  funcoppc4  49807  amgmwlem  50476  amgmlemALT  50477  amgmw2d  50478  young2d  50479