Theorem 3brtr3d 5122

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092

This theorem is referenced by:  ofrval  7622  difsnen  8972  domunsncan  8990  infdifsn  9547  ltaddnq  10862  lemul2a  11973  mul2lt0rlt0  12991  xleadd2a  13150  xlemul2a  13185  monoord2  13937  expubnd  14082  bernneq2  14134  hashfun  14341  01sqrexlem2  15147  abs2dif2  15238  rlimdiv  15550  isercolllem1  15569  iseraltlem2  15587  iseraltlem3  15588  fsum00  15702  seqabs  15718  cvgcmp  15720  mertenslem1  15788  fprodle  15900  eftlub  16015  eirrlem  16110  bitscmp  16346  prmreclem1  16825  invisoinvl  17694  chnind  18524  chnlt  18526  chnso  18527  ex-chn1  18540  efgcpbl2  19667  pgpfaclem2  19994  omndadd2d  20040  omndmul2  20043  omndmul3  20044  ogrpinv0le  20046  ogrpaddltbi  20049  ogrpaddltrbid  20051  ogrpinv0lt  20053  gsumle  20055  unitgrp  20299  orngsqr  20779  ornglmulle  20780  orngrmulle  20781  xblss2  24315  xmstri2  24379  mstri2  24380  xmstri  24381  mstri  24382  xmstri3  24383  mstri3  24384  msrtri  24385  nrmmetd  24487  nmtri  24539  nmoi2  24643  xrsxmet  24723  xrge0gsumle  24747  iccpnfhmeo  24868  pcorev2  24953  pi1cpbl  24969  rrxmet  25333  ovoliunlem1  25428  voliunlem3  25478  uniioombllem2  25509  dyadss  25520  dvlipcn  25924  dv11cn  25931  dvle  25937  dvfsumge  25953  dvfsumlem2  25958  dvfsumlem2OLD  25959  dvfsumlem4  25961  dvfsum2  25966  idomrootle  26103  dgrsub  26203  vieta1lem2  26244  itgulm2  26343  radcnvlem1  26347  abelthlem7  26373  efcvx  26384  logdivlti  26554  logcnlem4  26579  logccv  26597  cxple2a  26633  cxpaddlelem  26686  cxpaddle  26687  leibpi  26877  scvxcvx  26921  amgmlem  26925  logdiflbnd  26930  lgamgulmlem2  26965  lgamgulmlem5  26968  lgambdd  26972  lgamcvg2  26990  ftalem2  27009  ppip1le  27096  ppieq0  27111  ppiltx  27112  chpeq0  27144  chtublem  27147  chtub  27148  logexprlim  27161  perfectlem2  27166  bposlem9  27228  2sqlem8  27362  chebbnd1lem1  27405  vmadivsum  27418  rplogsumlem1  27420  dchrisum0re  27449  dchrisum0lem1  27452  selberglem2  27482  chpdifbndlem1  27489  selberg3lem1  27493  pntrlog2bndlem2  27514  pntrlog2bndlem3  27515  pntrlog2bndlem6  27519  pntpbnd2  27523  pntibndlem2  27527  pntlemb  27533  pntlemr  27538  pntlemo  27543  ostth2lem2  27570  ostth2lem3  27571  nosupbnd2lem1  27652  noinfbnd2lem1  27667  mulsgt0  28081  tgcgrsub2  28571  legso  28575  krippenlem  28666  midex  28713  opphllem3  28725  trgcopy  28780  occllem  31278  nmcexi  32001  cnlnadjlem7  32048  hmopidmchi  32126  oexpled  32825  mgcf1o  32979  isarchi3  33151  archirngz  33153  archiabllem1b  33156  isarchiofld  33163  cos9thpiminplylem1  33790  esum2d  34101  omssubadd  34308  carsgclctun  34329  eulerpartlemgc  34370  dstfrvclim1  34486  fdvneggt  34608  fdvnegge  34610  logdivsqrle  34658  hgt750lemb  34664  subfaclim  35220  ovoliunnfl  37701  itg2addnclem3  37712  ftc1anclem8  37739  cntotbnd  37835  rrnmet  37868  3atlem1  39521  3atlem2  39522  llncvrlpln2  39595  lplncvrlvol2  39653  dalem25  39736  dalawlem7  39915  dalawlem11  39919  cdleme22g  40386  cdlemg18b  40717  cdlemg46  40773  dia2dimlem3  41104  dihord2  41265  3lexlogpow5ineq2  42087  3lexlogpow2ineq1  42090  3lexlogpow5ineq5  42092  aks4d1p1p7  42106  aks4d1p1  42108  aks4d1p6  42113  aks6d1c2lem4  42159  sticksstones6  42183  bcled  42210  bcle2d  42211  aks6d1c7lem1  42212  jm2.24nn  42991  jm2.27a  43037  amgm2d  44230  amgm3d  44231  amgm4d  44232  binomcxplemrat  44382  binomcxplemnotnn0  44388  monoord2xrv  45520  ioossioobi  45556  ioodvbdlimc2lem  45971  stoweidlem10  46047  stoweidlem11  46048  stoweidlem13  46050  stoweidlem14  46051  stoweidlem28  46065  stirlinglem11  46121  stirlinglem12  46122  dirkercncflem4  46143  fourierdlem4  46148  fourierdlem6  46150  fourierdlem11  46155  fourierdlem42  46186  fourierdlem51  46194  fourierdlem73  46216  fourierdlem79  46222  2pwp1prm  47619  perfectALTVlem2  47752  fllogbd  48591  nnpw2blen  48611  funcoppc4  49175  amgmwlem  49833  amgmlemALT  49834  amgmw2d  49835  young2d  49836