Theorem 3brtr3d 5174

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  ofrval  7709  difsnen  9093  domunsncan  9112  phplem2OLD  9255  infdifsn  9697  ltaddnq  11014  lemul2a  12122  mul2lt0rlt0  13137  xleadd2a  13296  xlemul2a  13331  monoord2  14074  expubnd  14217  bernneq2  14269  hashfun  14476  01sqrexlem2  15282  abs2dif2  15372  rlimdiv  15682  isercolllem1  15701  iseraltlem2  15719  iseraltlem3  15720  fsum00  15834  seqabs  15850  cvgcmp  15852  mertenslem1  15920  fprodle  16032  eftlub  16145  eirrlem  16240  bitscmp  16475  prmreclem1  16954  invisoinvl  17834  efgcpbl2  19775  pgpfaclem2  20102  unitgrp  20383  xblss2  24412  xmstri2  24476  mstri2  24477  xmstri  24478  mstri  24479  xmstri3  24480  mstri3  24481  msrtri  24482  nrmmetd  24587  nmtri  24639  nmoi2  24751  xrsxmet  24831  xrge0gsumle  24855  iccpnfhmeo  24976  pcorev2  25061  pi1cpbl  25077  rrxmet  25442  ovoliunlem1  25537  voliunlem3  25587  uniioombllem2  25618  dyadss  25629  dvlipcn  26033  dv11cn  26040  dvle  26046  dvfsumge  26062  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem4  26070  dvfsum2  26075  idomrootle  26212  dgrsub  26312  vieta1lem2  26353  itgulm2  26452  radcnvlem1  26456  abelthlem7  26482  efcvx  26493  logdivlti  26662  logcnlem4  26687  logccv  26705  cxple2a  26741  cxpaddlelem  26794  cxpaddle  26795  leibpi  26985  scvxcvx  27029  amgmlem  27033  logdiflbnd  27038  lgamgulmlem2  27073  lgamgulmlem5  27076  lgambdd  27080  lgamcvg2  27098  ftalem2  27117  ppip1le  27204  ppieq0  27219  ppiltx  27220  chpeq0  27252  chtublem  27255  chtub  27256  logexprlim  27269  perfectlem2  27274  bposlem9  27336  2sqlem8  27470  chebbnd1lem1  27513  vmadivsum  27526  rplogsumlem1  27528  dchrisum0re  27557  dchrisum0lem1  27560  selberglem2  27590  chpdifbndlem1  27597  selberg3lem1  27601  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem6  27627  pntpbnd2  27631  pntibndlem2  27635  pntlemb  27641  pntlemr  27646  pntlemo  27651  ostth2lem2  27678  ostth2lem3  27679  nosupbnd2lem1  27760  noinfbnd2lem1  27775  mulsgt0  28170  tgcgrsub2  28603  legso  28607  krippenlem  28698  midex  28745  opphllem3  28757  trgcopy  28812  occllem  31322  nmcexi  32045  cnlnadjlem7  32092  hmopidmchi  32170  mgcf1o  32993  chnind  33001  chnlt  33003  chnso  33004  omndadd2d  33085  omndmul2  33089  omndmul3  33090  ogrpinv0le  33092  ogrpaddltbi  33095  ogrpaddltrbid  33097  ogrpinv0lt  33099  gsumle  33101  isarchi3  33194  archirngz  33196  archiabllem1b  33199  orngsqr  33334  ornglmulle  33335  orngrmulle  33336  isarchiofld  33347  esum2d  34094  omssubadd  34302  carsgclctun  34323  eulerpartlemgc  34364  dstfrvclim1  34480  fdvneggt  34615  fdvnegge  34617  logdivsqrle  34665  hgt750lemb  34671  subfaclim  35193  ovoliunnfl  37669  itg2addnclem3  37680  ftc1anclem8  37707  cntotbnd  37803  rrnmet  37836  3atlem1  39485  3atlem2  39486  llncvrlpln2  39559  lplncvrlvol2  39617  dalem25  39700  dalawlem7  39879  dalawlem11  39883  cdleme22g  40350  cdlemg18b  40681  cdlemg46  40737  dia2dimlem3  41068  dihord2  41229  3lexlogpow5ineq2  42056  3lexlogpow2ineq1  42059  3lexlogpow5ineq5  42061  aks4d1p1p7  42075  aks4d1p1  42077  aks4d1p6  42082  aks6d1c2lem4  42128  sticksstones6  42152  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  jm2.24nn  42971  jm2.27a  43017  amgm2d  44211  amgm3d  44212  amgm4d  44213  binomcxplemrat  44369  binomcxplemnotnn0  44375  monoord2xrv  45494  ioossioobi  45530  ioodvbdlimc2lem  45949  stoweidlem10  46025  stoweidlem11  46026  stoweidlem13  46028  stoweidlem14  46029  stoweidlem28  46043  stirlinglem11  46099  stirlinglem12  46100  dirkercncflem4  46121  fourierdlem4  46126  fourierdlem6  46128  fourierdlem11  46133  fourierdlem42  46164  fourierdlem51  46172  fourierdlem73  46194  fourierdlem79  46200  2pwp1prm  47576  perfectALTVlem2  47709  fllogbd  48481  nnpw2blen  48501  amgmwlem  49321  amgmlemALT  49322  amgmw2d  49323  young2d  49324