Theorem 3brtr3d 5131

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  ofrval  7644  difsnen  8999  domunsncan  9017  infdifsn  9578  ltaddnq  10897  lemul2a  12008  mul2lt0rlt0  13021  xleadd2a  13181  xlemul2a  13216  monoord2  13968  expubnd  14113  bernneq2  14165  hashfun  14372  01sqrexlem2  15178  abs2dif2  15269  rlimdiv  15581  isercolllem1  15600  iseraltlem2  15618  iseraltlem3  15619  fsum00  15733  seqabs  15749  cvgcmp  15751  mertenslem1  15819  fprodle  15931  eftlub  16046  eirrlem  16141  bitscmp  16377  prmreclem1  16856  invisoinvl  17726  chnind  18556  chnlt  18558  chnso  18559  ex-chn1  18572  efgcpbl2  19698  pgpfaclem2  20025  omndadd2d  20071  omndmul2  20074  omndmul3  20075  ogrpinv0le  20077  ogrpaddltbi  20080  ogrpaddltrbid  20082  ogrpinv0lt  20084  gsumle  20086  unitgrp  20331  orngsqr  20811  ornglmulle  20812  orngrmulle  20813  xblss2  24358  xmstri2  24422  mstri2  24423  xmstri  24424  mstri  24425  xmstri3  24426  mstri3  24427  msrtri  24428  nrmmetd  24530  nmtri  24582  nmoi2  24686  xrsxmet  24766  xrge0gsumle  24790  iccpnfhmeo  24911  pcorev2  24996  pi1cpbl  25012  rrxmet  25376  ovoliunlem1  25471  voliunlem3  25521  uniioombllem2  25552  dyadss  25563  dvlipcn  25967  dv11cn  25974  dvle  25980  dvfsumge  25996  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem4  26004  dvfsum2  26009  idomrootle  26146  dgrsub  26246  vieta1lem2  26287  itgulm2  26386  radcnvlem1  26390  abelthlem7  26416  efcvx  26427  logdivlti  26597  logcnlem4  26622  logccv  26640  cxple2a  26676  cxpaddlelem  26729  cxpaddle  26730  leibpi  26920  scvxcvx  26964  amgmlem  26968  logdiflbnd  26973  lgamgulmlem2  27008  lgamgulmlem5  27011  lgambdd  27015  lgamcvg2  27033  ftalem2  27052  ppip1le  27139  ppieq0  27154  ppiltx  27155  chpeq0  27187  chtublem  27190  chtub  27191  logexprlim  27204  perfectlem2  27209  bposlem9  27271  2sqlem8  27405  chebbnd1lem1  27448  vmadivsum  27461  rplogsumlem1  27463  dchrisum0re  27492  dchrisum0lem1  27495  selberglem2  27525  chpdifbndlem1  27532  selberg3lem1  27536  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem6  27562  pntpbnd2  27566  pntibndlem2  27570  pntlemb  27576  pntlemr  27581  pntlemo  27586  ostth2lem2  27613  ostth2lem3  27614  nosupbnd2lem1  27695  noinfbnd2lem1  27710  mulsgt0  28152  bdayfinbndlem1  28475  tgcgrsub2  28679  legso  28683  krippenlem  28774  midex  28821  opphllem3  28833  trgcopy  28888  occllem  31390  nmcexi  32113  cnlnadjlem7  32160  hmopidmchi  32238  oexpled  32938  mgcf1o  33095  isarchi3  33280  archirngz  33282  archiabllem1b  33285  isarchiofld  33292  cos9thpiminplylem1  33959  esum2d  34270  omssubadd  34477  carsgclctun  34498  eulerpartlemgc  34539  dstfrvclim1  34655  fdvneggt  34777  fdvnegge  34779  logdivsqrle  34827  hgt750lemb  34833  subfaclim  35401  ovoliunnfl  37907  itg2addnclem3  37918  ftc1anclem8  37945  cntotbnd  38041  rrnmet  38074  3atlem1  39853  3atlem2  39854  llncvrlpln2  39927  lplncvrlvol2  39985  dalem25  40068  dalawlem7  40247  dalawlem11  40251  cdleme22g  40718  cdlemg18b  41049  cdlemg46  41105  dia2dimlem3  41436  dihord2  41597  3lexlogpow5ineq2  42419  3lexlogpow2ineq1  42422  3lexlogpow5ineq5  42424  aks4d1p1p7  42438  aks4d1p1  42440  aks4d1p6  42445  aks6d1c2lem4  42491  sticksstones6  42515  bcled  42542  bcle2d  42543  aks6d1c7lem1  42544  jm2.24nn  43310  jm2.27a  43356  amgm2d  44548  amgm3d  44549  amgm4d  44550  binomcxplemrat  44700  binomcxplemnotnn0  44706  monoord2xrv  45835  ioossioobi  45871  ioodvbdlimc2lem  46286  stoweidlem10  46362  stoweidlem11  46363  stoweidlem13  46365  stoweidlem14  46366  stoweidlem28  46380  stirlinglem11  46436  stirlinglem12  46437  dirkercncflem4  46458  fourierdlem4  46463  fourierdlem6  46465  fourierdlem11  46470  fourierdlem42  46501  fourierdlem51  46509  fourierdlem73  46531  fourierdlem79  46537  chnerlem2  47235  2pwp1prm  47943  perfectALTVlem2  48076  fllogbd  48914  nnpw2blen  48934  funcoppc4  49497  amgmwlem  50155  amgmlemALT  50156  amgmw2d  50157  young2d  50158