Theorem 3brtr3d 5143

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

Syntax hints:   → wi 4   = wceq 1570   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111

This theorem is referenced by:  ofrval  7688  difsnen  9048  domunsncan  9066  infdifsn  9627  ltaddnq  10960  lemul2a  12071  mul2lt0rlt0  13121  xleadd2a  13281  xlemul2a  13316  monoord2  14071  expubnd  14216  bernneq2  14268  hashfun  14476  01sqrexlem2  15296  abs2dif2  15387  rlimdiv  15699  isercolllem1  15718  iseraltlem2  15736  iseraltlem3  15737  fsum00  15852  seqabs  15868  cvgcmp  15870  mertenslem1  15940  fprodle  16052  eftlub  16166  eirrlem  16261  bitscmp  16497  prmreclem1  16977  invisoinvl  17848  chnind  18678  chnlt  18680  chnso  18681  ex-chn1  18694  efgcpbl2  19828  pgpfaclem2  20155  omndadd2d  20201  omndmul2  20204  omndmul3  20205  ogrpinv0le  20207  ogrpaddltbi  20210  ogrpaddltrbid  20212  ogrpinv0lt  20214  gsumle  20216  unitgrp  20466  orngsqr  20950  ornglmulle  20951  orngrmulle  20952  xblss2  24540  xmstri2  24604  mstri2  24605  xmstri  24606  mstri  24607  xmstri3  24608  mstri3  24609  msrtri  24610  nrmmetd  24712  nmtri  24764  nmoi2  24868  xrsxmet  24948  xrge0gsumle  24972  iccpnfhmeo  25085  pcorev2  25168  pi1cpbl  25184  rrxmet  25548  ovoliunlem1  25642  voliunlem3  25692  uniioombllem2  25723  dyadss  25734  dvlipcn  26134  dv11cn  26141  dvle  26147  dvfsumge  26162  dvfsumlem2  26167  dvfsumlem4  26169  dvfsum2  26174  idomrootle  26311  dgrsub  26410  vieta1lem2  26453  itgulm2  26553  radcnvlem1  26557  abelthlem7  26582  efcvx  26593  logdivlti  26766  logcnlem4  26791  logccv  26809  cxple2a  26845  cxpaddlelem  26897  cxpaddle  26898  leibpi  27088  scvxcvx  27131  amgmlem  27135  logdiflbnd  27140  lgamgulmlem2  27175  lgamgulmlem5  27178  lgambdd  27182  lgamcvg2  27200  ftalem2  27219  ppip1le  27306  ppieq0  27321  ppiltx  27322  chpeq0  27353  chtublem  27356  chtub  27357  logexprlim  27370  perfectlem2  27375  bposlem9  27437  2sqlem8  27571  chebbnd1lem1  27614  vmadivsum  27627  rplogsumlem1  27629  dchrisum0re  27658  dchrisum0lem1  27661  selberglem2  27691  chpdifbndlem1  27698  selberg3lem1  27702  pntrlog2bndlem2  27723  pntrlog2bndlem3  27724  pntrlog2bndlem6  27728  pntpbnd2  27732  pntibndlem2  27736  pntlemb  27742  pntlemr  27747  pntlemo  27752  ostth2lem2  27779  ostth2lem3  27780  nosupbnd2lem1  27860  noinfbnd2lem1  27875  mulsgt0  28318  bdayfinbndlem1  28641  tgcgrsub2  28845  legso  28849  krippenlem  28948  midex  28999  opphllem3  29011  trgcopy  29096  perpeqlem  29131  occllem  31636  nmcexi  32359  cnlnadjlem7  32406  hmopidmchi  32484  oexpled  33161  mgcf1o  33304  isarchi3  33488  archirngz  33490  archiabllem1b  33493  isarchiofld  33500  cos9thpiminplylem1  34153  esum2d  34464  omssubadd  34671  carsgclctun  34692  eulerpartlemgc  34733  dstfrvclim1  34849  fdvneggt  34968  fdvnegge  34970  logdivsqrle  35018  hgt750lemb  35024  subfaclim  35661  ovoliunnfl  38294  itg2addnclem3  38305  ftc1anclem8  38332  cntotbnd  38428  rrnmet  38461  3atlem1  40238  3atlem2  40239  llncvrlpln2  40312  lplncvrlvol2  40370  dalem25  40453  dalawlem7  40632  dalawlem11  40636  cdleme22g  41103  cdlemg18b  41434  cdlemg46  41490  dia2dimlem3  41821  dihord2  41982  3lexlogpow5ineq2  42803  3lexlogpow2ineq1  42806  3lexlogpow5ineq5  42808  aks4d1p1p7  42822  aks4d1p1  42824  aks4d1p6  42829  aks6d1c2lem4  42875  sticksstones6  42899  bcled  42926  bcle2d  42927  aks6d1c7lem1  42928  jm2.24nn  43669  jm2.27a  43715  amgm2d  44907  amgm3d  44908  amgm4d  44909  binomcxplemrat  45043  binomcxplemnotnn0  45049  monoord2xrv  46180  ioossioobi  46216  ioodvbdlimc2lem  46631  stoweidlem10  46707  stoweidlem11  46708  stoweidlem13  46710  stoweidlem14  46711  stoweidlem28  46725  stirlinglem11  46781  stirlinglem12  46782  dirkercncflem4  46803  fourierdlem4  46808  fourierdlem6  46810  fourierdlem11  46815  fourierdlem42  46846  fourierdlem51  46854  fourierdlem73  46876  fourierdlem79  46882  chnerlem2  47582  2pwp1prm  48324  perfectALTVlem2  48470  fllogbd  49323  nnpw2blen  49343  funcoppc4  49905  amgmwlem  50585  amgmlemALT  50586  amgmw2d  50587  young2d  50588