Theorem 3brtr3d 5119

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5089

This theorem is referenced by:  ofrval  7616  difsnen  8966  domunsncan  8984  infdifsn  9541  ltaddnq  10856  lemul2a  11967  mul2lt0rlt0  12985  xleadd2a  13144  xlemul2a  13179  monoord2  13928  expubnd  14073  bernneq2  14125  hashfun  14332  01sqrexlem2  15137  abs2dif2  15228  rlimdiv  15540  isercolllem1  15559  iseraltlem2  15577  iseraltlem3  15578  fsum00  15692  seqabs  15708  cvgcmp  15710  mertenslem1  15778  fprodle  15890  eftlub  16005  eirrlem  16100  bitscmp  16336  prmreclem1  16815  invisoinvl  17684  efgcpbl2  19623  pgpfaclem2  19950  omndadd2d  19996  omndmul2  19999  omndmul3  20000  ogrpinv0le  20002  ogrpaddltbi  20005  ogrpaddltrbid  20007  ogrpinv0lt  20009  gsumle  20011  unitgrp  20255  orngsqr  20735  ornglmulle  20736  orngrmulle  20737  xblss2  24271  xmstri2  24335  mstri2  24336  xmstri  24337  mstri  24338  xmstri3  24339  mstri3  24340  msrtri  24341  nrmmetd  24443  nmtri  24495  nmoi2  24599  xrsxmet  24679  xrge0gsumle  24703  iccpnfhmeo  24824  pcorev2  24909  pi1cpbl  24925  rrxmet  25289  ovoliunlem1  25384  voliunlem3  25434  uniioombllem2  25465  dyadss  25476  dvlipcn  25880  dv11cn  25887  dvle  25893  dvfsumge  25909  dvfsumlem2  25914  dvfsumlem2OLD  25915  dvfsumlem4  25917  dvfsum2  25922  idomrootle  26059  dgrsub  26159  vieta1lem2  26200  itgulm2  26299  radcnvlem1  26303  abelthlem7  26329  efcvx  26340  logdivlti  26510  logcnlem4  26535  logccv  26553  cxple2a  26589  cxpaddlelem  26642  cxpaddle  26643  leibpi  26833  scvxcvx  26877  amgmlem  26881  logdiflbnd  26886  lgamgulmlem2  26921  lgamgulmlem5  26924  lgambdd  26928  lgamcvg2  26946  ftalem2  26965  ppip1le  27052  ppieq0  27067  ppiltx  27068  chpeq0  27100  chtublem  27103  chtub  27104  logexprlim  27117  perfectlem2  27122  bposlem9  27184  2sqlem8  27318  chebbnd1lem1  27361  vmadivsum  27374  rplogsumlem1  27376  dchrisum0re  27405  dchrisum0lem1  27408  selberglem2  27438  chpdifbndlem1  27445  selberg3lem1  27449  pntrlog2bndlem2  27470  pntrlog2bndlem3  27471  pntrlog2bndlem6  27475  pntpbnd2  27479  pntibndlem2  27483  pntlemb  27489  pntlemr  27494  pntlemo  27499  ostth2lem2  27526  ostth2lem3  27527  nosupbnd2lem1  27608  noinfbnd2lem1  27623  mulsgt0  28037  tgcgrsub2  28527  legso  28531  krippenlem  28622  midex  28669  opphllem3  28681  trgcopy  28736  occllem  31234  nmcexi  31957  cnlnadjlem7  32004  hmopidmchi  32082  oexpled  32785  mgcf1o  32940  chnind  32948  chnlt  32950  chnso  32951  isarchi3  33124  archirngz  33126  archiabllem1b  33129  isarchiofld  33136  cos9thpiminplylem1  33763  esum2d  34074  omssubadd  34281  carsgclctun  34302  eulerpartlemgc  34343  dstfrvclim1  34459  fdvneggt  34581  fdvnegge  34583  logdivsqrle  34631  hgt750lemb  34637  subfaclim  35178  ovoliunnfl  37659  itg2addnclem3  37670  ftc1anclem8  37697  cntotbnd  37793  rrnmet  37826  3atlem1  39479  3atlem2  39480  llncvrlpln2  39553  lplncvrlvol2  39611  dalem25  39694  dalawlem7  39873  dalawlem11  39877  cdleme22g  40344  cdlemg18b  40675  cdlemg46  40731  dia2dimlem3  41062  dihord2  41223  3lexlogpow5ineq2  42045  3lexlogpow2ineq1  42048  3lexlogpow5ineq5  42050  aks4d1p1p7  42064  aks4d1p1  42066  aks4d1p6  42071  aks6d1c2lem4  42117  sticksstones6  42141  bcled  42168  bcle2d  42169  aks6d1c7lem1  42170  jm2.24nn  42949  jm2.27a  42995  amgm2d  44188  amgm3d  44189  amgm4d  44190  binomcxplemrat  44340  binomcxplemnotnn0  44346  monoord2xrv  45478  ioossioobi  45514  ioodvbdlimc2lem  45929  stoweidlem10  46005  stoweidlem11  46006  stoweidlem13  46008  stoweidlem14  46009  stoweidlem28  46023  stirlinglem11  46079  stirlinglem12  46080  dirkercncflem4  46101  fourierdlem4  46106  fourierdlem6  46108  fourierdlem11  46113  fourierdlem42  46144  fourierdlem51  46152  fourierdlem73  46174  fourierdlem79  46180  2pwp1prm  47587  perfectALTVlem2  47720  fllogbd  48559  nnpw2blen  48579  funcoppc4  49143  amgmwlem  49801  amgmlemALT  49802  amgmw2d  49803  young2d  49804