Theorem 3brtr3d 5061

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

Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5030

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  ofrval  7399  difsnen  8582  domunsncan  8600  phplem2  8681  infdifsn  9104  ltaddnq  10385  lemul2a  11484  mul2lt0rlt0  12479  xleadd2a  12635  xlemul2a  12670  monoord2  13397  expubnd  13537  bernneq2  13587  hashfun  13794  sqrlem2  14595  abs2dif2  14685  rlimdiv  14994  isercolllem1  15013  iseraltlem2  15031  iseraltlem3  15032  fsum00  15145  seqabs  15161  cvgcmp  15163  mertenslem1  15232  fprodle  15342  eftlub  15454  eirrlem  15549  bitscmp  15777  prmreclem1  16242  invisoinvl  17052  efgcpbl2  18875  pgpfaclem2  19197  unitgrp  19413  xblss2  23009  xmstri2  23073  mstri2  23074  xmstri  23075  mstri  23076  xmstri3  23077  mstri3  23078  msrtri  23079  nrmmetd  23181  nmtri  23232  nmoi2  23336  xrsxmet  23414  xrge0gsumle  23438  iccpnfhmeo  23550  pcorev2  23633  pi1cpbl  23649  rrxmet  24012  ovoliunlem1  24106  voliunlem3  24156  uniioombllem2  24187  dyadss  24198  dvlipcn  24597  dv11cn  24604  dvle  24610  dvfsumge  24625  dvfsumlem2  24630  dvfsumlem4  24632  dvfsum2  24637  dgrsub  24869  vieta1lem2  24907  itgulm2  25004  radcnvlem1  25008  abelthlem7  25033  efcvx  25044  logdivlti  25211  logcnlem4  25236  logccv  25254  cxple2a  25290  cxpaddlelem  25340  cxpaddle  25341  leibpi  25528  scvxcvx  25571  amgmlem  25575  logdiflbnd  25580  lgamgulmlem2  25615  lgamgulmlem5  25618  lgambdd  25622  lgamcvg2  25640  ftalem2  25659  ppip1le  25746  ppieq0  25761  ppiltx  25762  chpeq0  25792  chtublem  25795  chtub  25796  logexprlim  25809  perfectlem2  25814  bposlem9  25876  2sqlem8  26010  chebbnd1lem1  26053  vmadivsum  26066  rplogsumlem1  26068  dchrisum0re  26097  dchrisum0lem1  26100  selberglem2  26130  chpdifbndlem1  26137  selberg3lem1  26141  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem6  26167  pntpbnd2  26171  pntibndlem2  26175  pntlemb  26181  pntlemr  26186  pntlemo  26191  ostth2lem2  26218  ostth2lem3  26219  tgcgrsub2  26389  legso  26393  krippenlem  26484  midex  26531  opphllem3  26543  trgcopy  26598  occllem  29086  nmcexi  29809  cnlnadjlem7  29856  hmopidmchi  29934  omndadd2d  30759  omndmul2  30763  omndmul3  30764  ogrpinv0le  30766  ogrpaddltbi  30769  ogrpaddltrbid  30771  ogrpinv0lt  30773  gsumle  30775  isarchi3  30866  archirngz  30868  archiabllem1b  30871  orngsqr  30928  ornglmulle  30929  orngrmulle  30930  isarchiofld  30941  esum2d  31462  omssubadd  31668  carsgclctun  31689  eulerpartlemgc  31730  dstfrvclim1  31845  fdvneggt  31981  fdvnegge  31983  logdivsqrle  32031  hgt750lemb  32037  subfaclim  32548  nosupbnd2lem1  33328  ovoliunnfl  35099  itg2addnclem3  35110  ftc1anclem8  35137  cntotbnd  35234  rrnmet  35267  3atlem1  36779  3atlem2  36780  llncvrlpln2  36853  lplncvrlvol2  36911  dalem25  36994  dalawlem7  37173  dalawlem11  37177  cdleme22g  37644  cdlemg18b  37975  cdlemg46  38031  dia2dimlem3  38362  dihord2  38523  jm2.24nn  39900  jm2.27a  39946  idomrootle  40139  amgm2d  40904  amgm3d  40905  amgm4d  40906  binomcxplemrat  41054  binomcxplemnotnn0  41060  monoord2xrv  42123  ioossioobi  42154  ioodvbdlimc2lem  42576  stoweidlem10  42652  stoweidlem11  42653  stoweidlem13  42655  stoweidlem14  42656  stoweidlem28  42670  stirlinglem11  42726  stirlinglem12  42727  dirkercncflem4  42748  fourierdlem4  42753  fourierdlem6  42755  fourierdlem11  42760  fourierdlem42  42791  fourierdlem51  42799  fourierdlem73  42821  fourierdlem79  42827  2pwp1prm  44106  perfectALTVlem2  44240  fllogbd  44974  nnpw2blen  44994  amgmwlem  45330  amgmlemALT  45331  amgmw2d  45332  young2d  45333