Theorem 3brtr3d 5138

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

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

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  ofrval  7665  difsnen  9023  domunsncan  9041  infdifsn  9610  ltaddnq  10927  lemul2a  12037  mul2lt0rlt0  13055  xleadd2a  13214  xlemul2a  13249  monoord2  13998  expubnd  14143  bernneq2  14195  hashfun  14402  01sqrexlem2  15209  abs2dif2  15300  rlimdiv  15612  isercolllem1  15631  iseraltlem2  15649  iseraltlem3  15650  fsum00  15764  seqabs  15780  cvgcmp  15782  mertenslem1  15850  fprodle  15962  eftlub  16077  eirrlem  16172  bitscmp  16408  prmreclem1  16887  invisoinvl  17752  efgcpbl2  19687  pgpfaclem2  20014  unitgrp  20292  xblss2  24290  xmstri2  24354  mstri2  24355  xmstri  24356  mstri  24357  xmstri3  24358  mstri3  24359  msrtri  24360  nrmmetd  24462  nmtri  24514  nmoi2  24618  xrsxmet  24698  xrge0gsumle  24722  iccpnfhmeo  24843  pcorev2  24928  pi1cpbl  24944  rrxmet  25308  ovoliunlem1  25403  voliunlem3  25453  uniioombllem2  25484  dyadss  25495  dvlipcn  25899  dv11cn  25906  dvle  25912  dvfsumge  25928  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem4  25936  dvfsum2  25941  idomrootle  26078  dgrsub  26178  vieta1lem2  26219  itgulm2  26318  radcnvlem1  26322  abelthlem7  26348  efcvx  26359  logdivlti  26529  logcnlem4  26554  logccv  26572  cxple2a  26608  cxpaddlelem  26661  cxpaddle  26662  leibpi  26852  scvxcvx  26896  amgmlem  26900  logdiflbnd  26905  lgamgulmlem2  26940  lgamgulmlem5  26943  lgambdd  26947  lgamcvg2  26965  ftalem2  26984  ppip1le  27071  ppieq0  27086  ppiltx  27087  chpeq0  27119  chtublem  27122  chtub  27123  logexprlim  27136  perfectlem2  27141  bposlem9  27203  2sqlem8  27337  chebbnd1lem1  27380  vmadivsum  27393  rplogsumlem1  27395  dchrisum0re  27424  dchrisum0lem1  27427  selberglem2  27457  chpdifbndlem1  27464  selberg3lem1  27468  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem6  27494  pntpbnd2  27498  pntibndlem2  27502  pntlemb  27508  pntlemr  27513  pntlemo  27518  ostth2lem2  27545  ostth2lem3  27546  nosupbnd2lem1  27627  noinfbnd2lem1  27642  mulsgt0  28047  tgcgrsub2  28522  legso  28526  krippenlem  28617  midex  28664  opphllem3  28676  trgcopy  28731  occllem  31232  nmcexi  31955  cnlnadjlem7  32002  hmopidmchi  32080  oexpled  32772  mgcf1o  32929  chnind  32937  chnlt  32939  chnso  32940  omndadd2d  33022  omndmul2  33026  omndmul3  33027  ogrpinv0le  33029  ogrpaddltbi  33032  ogrpaddltrbid  33034  ogrpinv0lt  33036  gsumle  33038  isarchi3  33141  archirngz  33143  archiabllem1b  33146  orngsqr  33282  ornglmulle  33283  orngrmulle  33284  isarchiofld  33295  cos9thpiminplylem1  33772  esum2d  34083  omssubadd  34291  carsgclctun  34312  eulerpartlemgc  34353  dstfrvclim1  34469  fdvneggt  34591  fdvnegge  34593  logdivsqrle  34641  hgt750lemb  34647  subfaclim  35175  ovoliunnfl  37656  itg2addnclem3  37667  ftc1anclem8  37694  cntotbnd  37790  rrnmet  37823  3atlem1  39477  3atlem2  39478  llncvrlpln2  39551  lplncvrlvol2  39609  dalem25  39692  dalawlem7  39871  dalawlem11  39875  cdleme22g  40342  cdlemg18b  40673  cdlemg46  40729  dia2dimlem3  41060  dihord2  41221  3lexlogpow5ineq2  42043  3lexlogpow2ineq1  42046  3lexlogpow5ineq5  42048  aks4d1p1p7  42062  aks4d1p1  42064  aks4d1p6  42069  aks6d1c2lem4  42115  sticksstones6  42139  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  jm2.24nn  42948  jm2.27a  42994  amgm2d  44187  amgm3d  44188  amgm4d  44189  binomcxplemrat  44339  binomcxplemnotnn0  44345  monoord2xrv  45479  ioossioobi  45515  ioodvbdlimc2lem  45932  stoweidlem10  46008  stoweidlem11  46009  stoweidlem13  46011  stoweidlem14  46012  stoweidlem28  46026  stirlinglem11  46082  stirlinglem12  46083  dirkercncflem4  46104  fourierdlem4  46109  fourierdlem6  46111  fourierdlem11  46116  fourierdlem42  46147  fourierdlem51  46155  fourierdlem73  46177  fourierdlem79  46183  2pwp1prm  47590  perfectALTVlem2  47723  fllogbd  48549  nnpw2blen  48569  funcoppc4  49133  amgmwlem  49791  amgmlemALT  49792  amgmw2d  49793  young2d  49794