Theorem 3brtr3d 5105

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075

This theorem is referenced by:  ofrval  7545  difsnen  8840  domunsncan  8859  phplem2OLD  9001  infdifsn  9415  ltaddnq  10730  lemul2a  11830  mul2lt0rlt0  12832  xleadd2a  12988  xlemul2a  13023  monoord2  13754  expubnd  13895  bernneq2  13945  hashfun  14152  sqrlem2  14955  abs2dif2  15045  rlimdiv  15357  isercolllem1  15376  iseraltlem2  15394  iseraltlem3  15395  fsum00  15510  seqabs  15526  cvgcmp  15528  mertenslem1  15596  fprodle  15706  eftlub  15818  eirrlem  15913  bitscmp  16145  prmreclem1  16617  invisoinvl  17502  efgcpbl2  19363  pgpfaclem2  19685  unitgrp  19909  xblss2  23555  xmstri2  23619  mstri2  23620  xmstri  23621  mstri  23622  xmstri3  23623  mstri3  23624  msrtri  23625  nrmmetd  23730  nmtri  23782  nmoi2  23894  xrsxmet  23972  xrge0gsumle  23996  iccpnfhmeo  24108  pcorev2  24191  pi1cpbl  24207  rrxmet  24572  ovoliunlem1  24666  voliunlem3  24716  uniioombllem2  24747  dyadss  24758  dvlipcn  25158  dv11cn  25165  dvle  25171  dvfsumge  25186  dvfsumlem2  25191  dvfsumlem4  25193  dvfsum2  25198  dgrsub  25433  vieta1lem2  25471  itgulm2  25568  radcnvlem1  25572  abelthlem7  25597  efcvx  25608  logdivlti  25775  logcnlem4  25800  logccv  25818  cxple2a  25854  cxpaddlelem  25904  cxpaddle  25905  leibpi  26092  scvxcvx  26135  amgmlem  26139  logdiflbnd  26144  lgamgulmlem2  26179  lgamgulmlem5  26182  lgambdd  26186  lgamcvg2  26204  ftalem2  26223  ppip1le  26310  ppieq0  26325  ppiltx  26326  chpeq0  26356  chtublem  26359  chtub  26360  logexprlim  26373  perfectlem2  26378  bposlem9  26440  2sqlem8  26574  chebbnd1lem1  26617  vmadivsum  26630  rplogsumlem1  26632  dchrisum0re  26661  dchrisum0lem1  26664  selberglem2  26694  chpdifbndlem1  26701  selberg3lem1  26705  pntrlog2bndlem2  26726  pntrlog2bndlem3  26727  pntrlog2bndlem6  26731  pntpbnd2  26735  pntibndlem2  26739  pntlemb  26745  pntlemr  26750  pntlemo  26755  ostth2lem2  26782  ostth2lem3  26783  tgcgrsub2  26956  legso  26960  krippenlem  27051  midex  27098  opphllem3  27110  trgcopy  27165  occllem  29665  nmcexi  30388  cnlnadjlem7  30435  hmopidmchi  30513  mgcf1o  31281  omndadd2d  31334  omndmul2  31338  omndmul3  31339  ogrpinv0le  31341  ogrpaddltbi  31344  ogrpaddltrbid  31346  ogrpinv0lt  31348  gsumle  31350  isarchi3  31441  archirngz  31443  archiabllem1b  31446  orngsqr  31503  ornglmulle  31504  orngrmulle  31505  isarchiofld  31516  esum2d  32061  omssubadd  32267  carsgclctun  32288  eulerpartlemgc  32329  dstfrvclim1  32444  fdvneggt  32580  fdvnegge  32582  logdivsqrle  32630  hgt750lemb  32636  subfaclim  33150  nosupbnd2lem1  33918  noinfbnd2lem1  33933  ovoliunnfl  35819  itg2addnclem3  35830  ftc1anclem8  35857  cntotbnd  35954  rrnmet  35987  3atlem1  37497  3atlem2  37498  llncvrlpln2  37571  lplncvrlvol2  37629  dalem25  37712  dalawlem7  37891  dalawlem11  37895  cdleme22g  38362  cdlemg18b  38693  cdlemg46  38749  dia2dimlem3  39080  dihord2  39241  3lexlogpow5ineq2  40063  3lexlogpow2ineq1  40066  3lexlogpow5ineq5  40068  aks4d1p1p7  40082  aks4d1p1  40084  aks4d1p6  40089  sticksstones6  40107  jm2.24nn  40781  jm2.27a  40827  idomrootle  41020  amgm2d  41809  amgm3d  41810  amgm4d  41811  binomcxplemrat  41968  binomcxplemnotnn0  41974  monoord2xrv  43024  ioossioobi  43055  ioodvbdlimc2lem  43475  stoweidlem10  43551  stoweidlem11  43552  stoweidlem13  43554  stoweidlem14  43555  stoweidlem28  43569  stirlinglem11  43625  stirlinglem12  43626  dirkercncflem4  43647  fourierdlem4  43652  fourierdlem6  43654  fourierdlem11  43659  fourierdlem42  43690  fourierdlem51  43698  fourierdlem73  43720  fourierdlem79  43726  2pwp1prm  45041  perfectALTVlem2  45174  fllogbd  45906  nnpw2blen  45926  amgmwlem  46506  amgmlemALT  46507  amgmw2d  46508  young2d  46509