Theorem 3brtr3d 5124

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

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

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094

This theorem is referenced by:  ofrval  7628  difsnen  8979  domunsncan  8997  infdifsn  9554  ltaddnq  10872  lemul2a  11983  mul2lt0rlt0  12996  xleadd2a  13155  xlemul2a  13190  monoord2  13942  expubnd  14087  bernneq2  14139  hashfun  14346  01sqrexlem2  15152  abs2dif2  15243  rlimdiv  15555  isercolllem1  15574  iseraltlem2  15592  iseraltlem3  15593  fsum00  15707  seqabs  15723  cvgcmp  15725  mertenslem1  15793  fprodle  15905  eftlub  16020  eirrlem  16115  bitscmp  16351  prmreclem1  16830  invisoinvl  17699  chnind  18529  chnlt  18531  chnso  18532  ex-chn1  18545  efgcpbl2  19671  pgpfaclem2  19998  omndadd2d  20044  omndmul2  20047  omndmul3  20048  ogrpinv0le  20050  ogrpaddltbi  20053  ogrpaddltrbid  20055  ogrpinv0lt  20057  gsumle  20059  unitgrp  20303  orngsqr  20783  ornglmulle  20784  orngrmulle  20785  xblss2  24318  xmstri2  24382  mstri2  24383  xmstri  24384  mstri  24385  xmstri3  24386  mstri3  24387  msrtri  24388  nrmmetd  24490  nmtri  24542  nmoi2  24646  xrsxmet  24726  xrge0gsumle  24750  iccpnfhmeo  24871  pcorev2  24956  pi1cpbl  24972  rrxmet  25336  ovoliunlem1  25431  voliunlem3  25481  uniioombllem2  25512  dyadss  25523  dvlipcn  25927  dv11cn  25934  dvle  25940  dvfsumge  25956  dvfsumlem2  25961  dvfsumlem2OLD  25962  dvfsumlem4  25964  dvfsum2  25969  idomrootle  26106  dgrsub  26206  vieta1lem2  26247  itgulm2  26346  radcnvlem1  26350  abelthlem7  26376  efcvx  26387  logdivlti  26557  logcnlem4  26582  logccv  26600  cxple2a  26636  cxpaddlelem  26689  cxpaddle  26690  leibpi  26880  scvxcvx  26924  amgmlem  26928  logdiflbnd  26933  lgamgulmlem2  26968  lgamgulmlem5  26971  lgambdd  26975  lgamcvg2  26993  ftalem2  27012  ppip1le  27099  ppieq0  27114  ppiltx  27115  chpeq0  27147  chtublem  27150  chtub  27151  logexprlim  27164  perfectlem2  27169  bposlem9  27231  2sqlem8  27365  chebbnd1lem1  27408  vmadivsum  27421  rplogsumlem1  27423  dchrisum0re  27452  dchrisum0lem1  27455  selberglem2  27485  chpdifbndlem1  27492  selberg3lem1  27496  pntrlog2bndlem2  27517  pntrlog2bndlem3  27518  pntrlog2bndlem6  27522  pntpbnd2  27526  pntibndlem2  27530  pntlemb  27536  pntlemr  27541  pntlemo  27546  ostth2lem2  27573  ostth2lem3  27574  nosupbnd2lem1  27655  noinfbnd2lem1  27670  mulsgt0  28084  tgcgrsub2  28574  legso  28578  krippenlem  28669  midex  28716  opphllem3  28728  trgcopy  28783  occllem  31285  nmcexi  32008  cnlnadjlem7  32055  hmopidmchi  32133  oexpled  32835  mgcf1o  32991  isarchi3  33163  archirngz  33165  archiabllem1b  33168  isarchiofld  33175  cos9thpiminplylem1  33816  esum2d  34127  omssubadd  34334  carsgclctun  34355  eulerpartlemgc  34396  dstfrvclim1  34512  fdvneggt  34634  fdvnegge  34636  logdivsqrle  34684  hgt750lemb  34690  subfaclim  35253  ovoliunnfl  37722  itg2addnclem3  37733  ftc1anclem8  37760  cntotbnd  37856  rrnmet  37889  3atlem1  39602  3atlem2  39603  llncvrlpln2  39676  lplncvrlvol2  39734  dalem25  39817  dalawlem7  39996  dalawlem11  40000  cdleme22g  40467  cdlemg18b  40798  cdlemg46  40854  dia2dimlem3  41185  dihord2  41346  3lexlogpow5ineq2  42168  3lexlogpow2ineq1  42171  3lexlogpow5ineq5  42173  aks4d1p1p7  42187  aks4d1p1  42189  aks4d1p6  42194  aks6d1c2lem4  42240  sticksstones6  42264  bcled  42291  bcle2d  42292  aks6d1c7lem1  42293  jm2.24nn  43076  jm2.27a  43122  amgm2d  44315  amgm3d  44316  amgm4d  44317  binomcxplemrat  44467  binomcxplemnotnn0  44473  monoord2xrv  45605  ioossioobi  45641  ioodvbdlimc2lem  46056  stoweidlem10  46132  stoweidlem11  46133  stoweidlem13  46135  stoweidlem14  46136  stoweidlem28  46150  stirlinglem11  46206  stirlinglem12  46207  dirkercncflem4  46228  fourierdlem4  46233  fourierdlem6  46235  fourierdlem11  46240  fourierdlem42  46271  fourierdlem51  46279  fourierdlem73  46301  fourierdlem79  46307  chnerlem2  47005  2pwp1prm  47713  perfectALTVlem2  47846  fllogbd  48685  nnpw2blen  48705  funcoppc4  49269  amgmwlem  49927  amgmlemALT  49928  amgmw2d  49929  young2d  49930