Theorem 3brtr3d 5179

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

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

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  ofrval  7679  difsnen  9050  domunsncan  9069  phplem2OLD  9215  infdifsn  9649  ltaddnq  10966  lemul2a  12066  mul2lt0rlt0  13073  xleadd2a  13230  xlemul2a  13265  monoord2  13996  expubnd  14139  bernneq2  14190  hashfun  14394  01sqrexlem2  15187  abs2dif2  15277  rlimdiv  15589  isercolllem1  15608  iseraltlem2  15626  iseraltlem3  15627  fsum00  15741  seqabs  15757  cvgcmp  15759  mertenslem1  15827  fprodle  15937  eftlub  16049  eirrlem  16144  bitscmp  16376  prmreclem1  16846  invisoinvl  17734  efgcpbl2  19620  pgpfaclem2  19947  unitgrp  20190  xblss2  23900  xmstri2  23964  mstri2  23965  xmstri  23966  mstri  23967  xmstri3  23968  mstri3  23969  msrtri  23970  nrmmetd  24075  nmtri  24127  nmoi2  24239  xrsxmet  24317  xrge0gsumle  24341  iccpnfhmeo  24453  pcorev2  24536  pi1cpbl  24552  rrxmet  24917  ovoliunlem1  25011  voliunlem3  25061  uniioombllem2  25092  dyadss  25103  dvlipcn  25503  dv11cn  25510  dvle  25516  dvfsumge  25531  dvfsumlem2  25536  dvfsumlem4  25538  dvfsum2  25543  dgrsub  25778  vieta1lem2  25816  itgulm2  25913  radcnvlem1  25917  abelthlem7  25942  efcvx  25953  logdivlti  26120  logcnlem4  26145  logccv  26163  cxple2a  26199  cxpaddlelem  26249  cxpaddle  26250  leibpi  26437  scvxcvx  26480  amgmlem  26484  logdiflbnd  26489  lgamgulmlem2  26524  lgamgulmlem5  26527  lgambdd  26531  lgamcvg2  26549  ftalem2  26568  ppip1le  26655  ppieq0  26670  ppiltx  26671  chpeq0  26701  chtublem  26704  chtub  26705  logexprlim  26718  perfectlem2  26723  bposlem9  26785  2sqlem8  26919  chebbnd1lem1  26962  vmadivsum  26975  rplogsumlem1  26977  dchrisum0re  27006  dchrisum0lem1  27009  selberglem2  27039  chpdifbndlem1  27046  selberg3lem1  27050  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem6  27076  pntpbnd2  27080  pntibndlem2  27084  pntlemb  27090  pntlemr  27095  pntlemo  27100  ostth2lem2  27127  ostth2lem3  27128  nosupbnd2lem1  27208  noinfbnd2lem1  27223  mulsgt0  27590  tgcgrsub2  27836  legso  27840  krippenlem  27931  midex  27978  opphllem3  27990  trgcopy  28045  occllem  30544  nmcexi  31267  cnlnadjlem7  31314  hmopidmchi  31392  mgcf1o  32161  omndadd2d  32214  omndmul2  32218  omndmul3  32219  ogrpinv0le  32221  ogrpaddltbi  32224  ogrpaddltrbid  32226  ogrpinv0lt  32228  gsumle  32230  isarchi3  32321  archirngz  32323  archiabllem1b  32326  orngsqr  32411  ornglmulle  32412  orngrmulle  32413  isarchiofld  32424  esum2d  33080  omssubadd  33288  carsgclctun  33309  eulerpartlemgc  33350  dstfrvclim1  33465  fdvneggt  33601  fdvnegge  33603  logdivsqrle  33651  hgt750lemb  33657  subfaclim  34168  gg-dvfsumlem2  35172  ovoliunnfl  36519  itg2addnclem3  36530  ftc1anclem8  36557  cntotbnd  36653  rrnmet  36686  3atlem1  38343  3atlem2  38344  llncvrlpln2  38417  lplncvrlvol2  38475  dalem25  38558  dalawlem7  38737  dalawlem11  38741  cdleme22g  39208  cdlemg18b  39539  cdlemg46  39595  dia2dimlem3  39926  dihord2  40087  3lexlogpow5ineq2  40909  3lexlogpow2ineq1  40912  3lexlogpow5ineq5  40914  aks4d1p1p7  40928  aks4d1p1  40930  aks4d1p6  40935  sticksstones6  40956  jm2.24nn  41684  jm2.27a  41730  idomrootle  41923  amgm2d  42936  amgm3d  42937  amgm4d  42938  binomcxplemrat  43095  binomcxplemnotnn0  43101  monoord2xrv  44181  ioossioobi  44217  ioodvbdlimc2lem  44637  stoweidlem10  44713  stoweidlem11  44714  stoweidlem13  44716  stoweidlem14  44717  stoweidlem28  44731  stirlinglem11  44787  stirlinglem12  44788  dirkercncflem4  44809  fourierdlem4  44814  fourierdlem6  44816  fourierdlem11  44821  fourierdlem42  44852  fourierdlem51  44860  fourierdlem73  44882  fourierdlem79  44888  2pwp1prm  46244  perfectALTVlem2  46377  fllogbd  47200  nnpw2blen  47220  amgmwlem  47803  amgmlemALT  47804  amgmw2d  47805  young2d  47806