Theorem 3brtr3d 5117

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  ofrval  7636  difsnen  8990  domunsncan  9008  infdifsn  9569  ltaddnq  10888  lemul2a  12001  mul2lt0rlt0  13037  xleadd2a  13197  xlemul2a  13232  monoord2  13986  expubnd  14131  bernneq2  14183  hashfun  14390  01sqrexlem2  15196  abs2dif2  15287  rlimdiv  15599  isercolllem1  15618  iseraltlem2  15636  iseraltlem3  15637  fsum00  15752  seqabs  15768  cvgcmp  15770  mertenslem1  15840  fprodle  15952  eftlub  16067  eirrlem  16162  bitscmp  16398  prmreclem1  16878  invisoinvl  17748  chnind  18578  chnlt  18580  chnso  18581  ex-chn1  18594  efgcpbl2  19723  pgpfaclem2  20050  omndadd2d  20096  omndmul2  20099  omndmul3  20100  ogrpinv0le  20102  ogrpaddltbi  20105  ogrpaddltrbid  20107  ogrpinv0lt  20109  gsumle  20111  unitgrp  20354  orngsqr  20834  ornglmulle  20835  orngrmulle  20836  xblss2  24377  xmstri2  24441  mstri2  24442  xmstri  24443  mstri  24444  xmstri3  24445  mstri3  24446  msrtri  24447  nrmmetd  24549  nmtri  24601  nmoi2  24705  xrsxmet  24785  xrge0gsumle  24809  iccpnfhmeo  24922  pcorev2  25005  pi1cpbl  25021  rrxmet  25385  ovoliunlem1  25479  voliunlem3  25529  uniioombllem2  25560  dyadss  25571  dvlipcn  25971  dv11cn  25978  dvle  25984  dvfsumge  25999  dvfsumlem2  26004  dvfsumlem4  26006  dvfsum2  26011  idomrootle  26148  dgrsub  26247  vieta1lem2  26288  itgulm2  26387  radcnvlem1  26391  abelthlem7  26416  efcvx  26427  logdivlti  26597  logcnlem4  26622  logccv  26640  cxple2a  26676  cxpaddlelem  26728  cxpaddle  26729  leibpi  26919  scvxcvx  26963  amgmlem  26967  logdiflbnd  26972  lgamgulmlem2  27007  lgamgulmlem5  27010  lgambdd  27014  lgamcvg2  27032  ftalem2  27051  ppip1le  27138  ppieq0  27153  ppiltx  27154  chpeq0  27185  chtublem  27188  chtub  27189  logexprlim  27202  perfectlem2  27207  bposlem9  27269  2sqlem8  27403  chebbnd1lem1  27446  vmadivsum  27459  rplogsumlem1  27461  dchrisum0re  27490  dchrisum0lem1  27493  selberglem2  27523  chpdifbndlem1  27530  selberg3lem1  27534  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem6  27560  pntpbnd2  27564  pntibndlem2  27568  pntlemb  27574  pntlemr  27579  pntlemo  27584  ostth2lem2  27611  ostth2lem3  27612  nosupbnd2lem1  27693  noinfbnd2lem1  27708  mulsgt0  28150  bdayfinbndlem1  28473  tgcgrsub2  28677  legso  28681  krippenlem  28772  midex  28819  opphllem3  28831  trgcopy  28886  occllem  31389  nmcexi  32112  cnlnadjlem7  32159  hmopidmchi  32237  oexpled  32935  mgcf1o  33078  isarchi3  33263  archirngz  33265  archiabllem1b  33268  isarchiofld  33275  cos9thpiminplylem1  33942  esum2d  34253  omssubadd  34460  carsgclctun  34481  eulerpartlemgc  34522  dstfrvclim1  34638  fdvneggt  34760  fdvnegge  34762  logdivsqrle  34810  hgt750lemb  34816  subfaclim  35386  ovoliunnfl  37997  itg2addnclem3  38008  ftc1anclem8  38035  cntotbnd  38131  rrnmet  38164  3atlem1  39943  3atlem2  39944  llncvrlpln2  40017  lplncvrlvol2  40075  dalem25  40158  dalawlem7  40337  dalawlem11  40341  cdleme22g  40808  cdlemg18b  41139  cdlemg46  41195  dia2dimlem3  41526  dihord2  41687  3lexlogpow5ineq2  42508  3lexlogpow2ineq1  42511  3lexlogpow5ineq5  42513  aks4d1p1p7  42527  aks4d1p1  42529  aks4d1p6  42534  aks6d1c2lem4  42580  sticksstones6  42604  bcled  42631  bcle2d  42632  aks6d1c7lem1  42633  jm2.24nn  43405  jm2.27a  43451  amgm2d  44643  amgm3d  44644  amgm4d  44645  binomcxplemrat  44795  binomcxplemnotnn0  44801  monoord2xrv  45929  ioossioobi  45965  ioodvbdlimc2lem  46380  stoweidlem10  46456  stoweidlem11  46457  stoweidlem13  46459  stoweidlem14  46460  stoweidlem28  46474  stirlinglem11  46530  stirlinglem12  46531  dirkercncflem4  46552  fourierdlem4  46557  fourierdlem6  46559  fourierdlem11  46564  fourierdlem42  46595  fourierdlem51  46603  fourierdlem73  46625  fourierdlem79  46631  chnerlem2  47329  2pwp1prm  48064  perfectALTVlem2  48210  fllogbd  49048  nnpw2blen  49068  funcoppc4  49631  amgmwlem  50289  amgmlemALT  50290  amgmw2d  50291  young2d  50292