Theorem 3brtr3d 5110

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

Syntax hints:   → wi 4   = wceq 1547   class class class wbr 5079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080

This theorem is referenced by:  ofrval  7639  difsnen  8994  domunsncan  9012  infdifsn  9576  ltaddnq  10895  lemul2a  12008  mul2lt0rlt0  13044  xleadd2a  13204  xlemul2a  13239  monoord2  13993  expubnd  14138  bernneq2  14190  hashfun  14397  01sqrexlem2  15203  abs2dif2  15294  rlimdiv  15606  isercolllem1  15625  iseraltlem2  15643  iseraltlem3  15644  fsum00  15759  seqabs  15775  cvgcmp  15777  mertenslem1  15847  fprodle  15959  eftlub  16074  eirrlem  16169  bitscmp  16405  prmreclem1  16885  invisoinvl  17755  chnind  18585  chnlt  18587  chnso  18588  ex-chn1  18601  efgcpbl2  19730  pgpfaclem2  20057  omndadd2d  20103  omndmul2  20106  omndmul3  20107  ogrpinv0le  20109  ogrpaddltbi  20112  ogrpaddltrbid  20114  ogrpinv0lt  20116  gsumle  20118  unitgrp  20361  orngsqr  20845  ornglmulle  20846  orngrmulle  20847  xblss2  24392  xmstri2  24456  mstri2  24457  xmstri  24458  mstri  24459  xmstri3  24460  mstri3  24461  msrtri  24462  nrmmetd  24564  nmtri  24616  nmoi2  24720  xrsxmet  24800  xrge0gsumle  24824  iccpnfhmeo  24937  pcorev2  25020  pi1cpbl  25036  rrxmet  25400  ovoliunlem1  25494  voliunlem3  25544  uniioombllem2  25575  dyadss  25586  dvlipcn  25986  dv11cn  25993  dvle  25999  dvfsumge  26014  dvfsumlem2  26019  dvfsumlem4  26021  dvfsum2  26026  idomrootle  26163  dgrsub  26262  vieta1lem2  26302  itgulm2  26399  radcnvlem1  26403  abelthlem7  26428  efcvx  26439  logdivlti  26609  logcnlem4  26634  logccv  26652  cxple2a  26688  cxpaddlelem  26740  cxpaddle  26741  leibpi  26931  scvxcvx  26974  amgmlem  26978  logdiflbnd  26983  lgamgulmlem2  27018  lgamgulmlem5  27021  lgambdd  27025  lgamcvg2  27043  ftalem2  27062  ppip1le  27149  ppieq0  27164  ppiltx  27165  chpeq0  27196  chtublem  27199  chtub  27200  logexprlim  27213  perfectlem2  27218  bposlem9  27280  2sqlem8  27414  chebbnd1lem1  27457  vmadivsum  27470  rplogsumlem1  27472  dchrisum0re  27501  dchrisum0lem1  27504  selberglem2  27534  chpdifbndlem1  27541  selberg3lem1  27545  pntrlog2bndlem2  27566  pntrlog2bndlem3  27567  pntrlog2bndlem6  27571  pntpbnd2  27575  pntibndlem2  27579  pntlemb  27585  pntlemr  27590  pntlemo  27595  ostth2lem2  27622  ostth2lem3  27623  nosupbnd2lem1  27704  noinfbnd2lem1  27719  mulsgt0  28161  bdayfinbndlem1  28484  tgcgrsub2  28688  legso  28692  krippenlem  28783  midex  28830  opphllem3  28842  trgcopy  28897  occllem  31399  nmcexi  32122  cnlnadjlem7  32169  hmopidmchi  32247  oexpled  32946  mgcf1o  33089  isarchi3  33275  archirngz  33277  archiabllem1b  33280  isarchiofld  33287  cos9thpiminplylem1  33973  esum2d  34284  omssubadd  34491  carsgclctun  34512  eulerpartlemgc  34553  dstfrvclim1  34669  fdvneggt  34791  fdvnegge  34793  logdivsqrle  34841  hgt750lemb  34847  subfaclim  35423  ovoliunnfl  38036  itg2addnclem3  38047  ftc1anclem8  38074  cntotbnd  38170  rrnmet  38203  3atlem1  39982  3atlem2  39983  llncvrlpln2  40056  lplncvrlvol2  40114  dalem25  40197  dalawlem7  40376  dalawlem11  40380  cdleme22g  40847  cdlemg18b  41178  cdlemg46  41234  dia2dimlem3  41565  dihord2  41726  3lexlogpow5ineq2  42547  3lexlogpow2ineq1  42550  3lexlogpow5ineq5  42552  aks4d1p1p7  42566  aks4d1p1  42568  aks4d1p6  42573  aks6d1c2lem4  42619  sticksstones6  42643  bcled  42670  bcle2d  42671  aks6d1c7lem1  42672  jm2.24nn  43411  jm2.27a  43457  amgm2d  44649  amgm3d  44650  amgm4d  44651  binomcxplemrat  44801  binomcxplemnotnn0  44807  monoord2xrv  45933  ioossioobi  45969  ioodvbdlimc2lem  46384  stoweidlem10  46460  stoweidlem11  46461  stoweidlem13  46463  stoweidlem14  46464  stoweidlem28  46478  stirlinglem11  46534  stirlinglem12  46535  dirkercncflem4  46556  fourierdlem4  46561  fourierdlem6  46563  fourierdlem11  46568  fourierdlem42  46599  fourierdlem51  46607  fourierdlem73  46629  fourierdlem79  46635  chnerlem2  47335  2pwp1prm  48074  perfectALTVlem2  48220  fllogbd  49058  nnpw2blen  49078  funcoppc4  49641  amgmwlem  50299  amgmlemALT  50300  amgmw2d  50301  young2d  50302