Theorem 3brtr3d 5197

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  ofrval  7726  difsnen  9119  domunsncan  9138  phplem2OLD  9281  infdifsn  9726  ltaddnq  11043  lemul2a  12149  mul2lt0rlt0  13159  xleadd2a  13316  xlemul2a  13351  monoord2  14084  expubnd  14227  bernneq2  14279  hashfun  14486  01sqrexlem2  15292  abs2dif2  15382  rlimdiv  15694  isercolllem1  15713  iseraltlem2  15731  iseraltlem3  15732  fsum00  15846  seqabs  15862  cvgcmp  15864  mertenslem1  15932  fprodle  16044  eftlub  16157  eirrlem  16252  bitscmp  16484  prmreclem1  16963  invisoinvl  17851  efgcpbl2  19799  pgpfaclem2  20126  unitgrp  20409  xblss2  24433  xmstri2  24497  mstri2  24498  xmstri  24499  mstri  24500  xmstri3  24501  mstri3  24502  msrtri  24503  nrmmetd  24608  nmtri  24660  nmoi2  24772  xrsxmet  24850  xrge0gsumle  24874  iccpnfhmeo  24995  pcorev2  25080  pi1cpbl  25096  rrxmet  25461  ovoliunlem1  25556  voliunlem3  25606  uniioombllem2  25637  dyadss  25648  dvlipcn  26053  dv11cn  26060  dvle  26066  dvfsumge  26082  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem4  26090  dvfsum2  26095  idomrootle  26232  dgrsub  26332  vieta1lem2  26371  itgulm2  26470  radcnvlem1  26474  abelthlem7  26500  efcvx  26511  logdivlti  26680  logcnlem4  26705  logccv  26723  cxple2a  26759  cxpaddlelem  26812  cxpaddle  26813  leibpi  27003  scvxcvx  27047  amgmlem  27051  logdiflbnd  27056  lgamgulmlem2  27091  lgamgulmlem5  27094  lgambdd  27098  lgamcvg2  27116  ftalem2  27135  ppip1le  27222  ppieq0  27237  ppiltx  27238  chpeq0  27270  chtublem  27273  chtub  27274  logexprlim  27287  perfectlem2  27292  bposlem9  27354  2sqlem8  27488  chebbnd1lem1  27531  vmadivsum  27544  rplogsumlem1  27546  dchrisum0re  27575  dchrisum0lem1  27578  selberglem2  27608  chpdifbndlem1  27615  selberg3lem1  27619  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem6  27645  pntpbnd2  27649  pntibndlem2  27653  pntlemb  27659  pntlemr  27664  pntlemo  27669  ostth2lem2  27696  ostth2lem3  27697  nosupbnd2lem1  27778  noinfbnd2lem1  27793  mulsgt0  28188  tgcgrsub2  28621  legso  28625  krippenlem  28716  midex  28763  opphllem3  28775  trgcopy  28830  occllem  31335  nmcexi  32058  cnlnadjlem7  32105  hmopidmchi  32183  mgcf1o  32976  chnind  32983  chnlt  32985  chnso  32986  omndadd2d  33058  omndmul2  33062  omndmul3  33063  ogrpinv0le  33065  ogrpaddltbi  33068  ogrpaddltrbid  33070  ogrpinv0lt  33072  gsumle  33074  isarchi3  33167  archirngz  33169  archiabllem1b  33172  orngsqr  33299  ornglmulle  33300  orngrmulle  33301  isarchiofld  33312  esum2d  34057  omssubadd  34265  carsgclctun  34286  eulerpartlemgc  34327  dstfrvclim1  34442  fdvneggt  34577  fdvnegge  34579  logdivsqrle  34627  hgt750lemb  34633  subfaclim  35156  ovoliunnfl  37622  itg2addnclem3  37633  ftc1anclem8  37660  cntotbnd  37756  rrnmet  37789  3atlem1  39440  3atlem2  39441  llncvrlpln2  39514  lplncvrlvol2  39572  dalem25  39655  dalawlem7  39834  dalawlem11  39838  cdleme22g  40305  cdlemg18b  40636  cdlemg46  40692  dia2dimlem3  41023  dihord2  41184  3lexlogpow5ineq2  42012  3lexlogpow2ineq1  42015  3lexlogpow5ineq5  42017  aks4d1p1p7  42031  aks4d1p1  42033  aks4d1p6  42038  aks6d1c2lem4  42084  sticksstones6  42108  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  jm2.24nn  42916  jm2.27a  42962  amgm2d  44160  amgm3d  44161  amgm4d  44162  binomcxplemrat  44319  binomcxplemnotnn0  44325  monoord2xrv  45399  ioossioobi  45435  ioodvbdlimc2lem  45855  stoweidlem10  45931  stoweidlem11  45932  stoweidlem13  45934  stoweidlem14  45935  stoweidlem28  45949  stirlinglem11  46005  stirlinglem12  46006  dirkercncflem4  46027  fourierdlem4  46032  fourierdlem6  46034  fourierdlem11  46039  fourierdlem42  46070  fourierdlem51  46078  fourierdlem73  46100  fourierdlem79  46106  2pwp1prm  47463  perfectALTVlem2  47596  fllogbd  48294  nnpw2blen  48314  amgmwlem  48896  amgmlemALT  48897  amgmw2d  48898  young2d  48899