Theorem 3brtr4d 5180

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)

Hypotheses

Ref	Expression
3brtr4d.1	⊢ (𝜑 → 𝐴𝑅𝐵)
3brtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3brtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3brtr4d	⊢ (𝜑 → 𝐶𝑅𝐷)

Proof of Theorem 3brtr4d

Step	Hyp	Ref	Expression
1		3brtr4d.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		3brtr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3		3brtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
4	2, 3	breq12d 5161	. 2 ⊢ (𝜑 → (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵))
5	1, 4	mpbird 257	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:  f1oiso2  7346  sucdom2OLD  9079  sucdom2  9203  ordtypelem6  9515  ttrcltr  9708  ttrclss  9712  ttrclselem2  9718  fin23lem26  10317  distrnq  10953  lediv12a  12104  recp1lt1  12109  ifle  13173  xleadd1a  13229  xlemul1a  13264  fldiv4p1lem1div2  13797  fldiv4lem1div2  13799  quoremz  13817  quoremnn0ALT  13819  intfracq  13821  modmulnn  13851  fzennn  13930  monoord2  13996  expgt1  14063  expmordi  14129  leexp2r  14136  leexp1a  14137  bernneq  14189  expmulnbnd  14195  digit1  14197  faclbnd  14247  faclbnd4lem3  14252  faclbnd4lem4  14253  faclbnd6  14256  facubnd  14257  hashdomi  14337  fzsdom2  14385  absrele  15252  absimle  15253  abstri  15274  abs2difabs  15278  limsupval2  15421  rlimrege0  15520  rlimrecl  15521  climsqz  15582  climsqz2  15583  rlimdiv  15589  rlimsqz  15593  rlimsqz2  15594  isercolllem1  15608  isercoll2  15612  fsumcvg2  15670  fsumrlim  15754  o1fsum  15756  cvgcmpce  15761  isumle  15787  climcndslem1  15792  climcndslem2  15793  harmonic  15802  expcnv  15807  explecnv  15808  geomulcvg  15819  efcllem  16018  ege2le3  16030  eflegeo  16061  rpnnen2lem4  16157  ruclem2  16172  ruclem8  16177  fsumdvds  16248  phibnd  16701  iserodd  16765  pcdvdstr  16806  pcprmpw2  16812  pockthg  16836  prmreclem4  16849  prmolefac  16976  2expltfac  17023  mod2ile  18444  odsubdvds  19434  pgpfi  19468  fislw  19488  efgredlemd  19607  efgredlem  19610  frgpcpbl  19622  abvres  20440  abvtrivd  20441  znrrg  21113  cstucnd  23781  psmetge0  23810  psmetres2  23812  xmetge0  23842  xmetres2  23859  imasf1oxmet  23873  comet  24014  stdbdxmet  24016  dscmet  24073  nrmmetd  24075  nmrtri  24125  tngngp  24163  nmolb2d  24227  nmoleub  24240  nmoco  24246  nmotri  24248  nmoid  24251  nmods  24253  cnmet  24280  xrsxmet  24317  metdstri  24359  metnrmlem3  24369  lebnumlem3  24471  ipcau2  24743  tcphcphlem1  24744  tcphcph  24746  trirn  24909  rrxmet  24917  rrxdstprj1  24918  minveclem2  24935  ovolunlem1a  25005  ovolscalem1  25022  volss  25042  voliunlem1  25059  volcn  25115  itg1climres  25224  mbfi1fseqlem5  25229  mbfi1fseqlem6  25230  itg2const2  25251  itg2seq  25252  itg2mulc  25257  itg2splitlem  25258  itg2monolem1  25260  itg2i1fseqle  25264  itg2i1fseq  25265  itg2i1fseq2  25266  itg2addlem  25268  itg2cnlem1  25271  itg2cnlem2  25272  iblss  25314  itgle  25319  ibladdlem  25329  iblabs  25338  iblabsr  25339  iblmulc2  25340  itgabs  25344  bddmulibl  25348  bddiblnc  25351  dvfsumabs  25532  dvfsumlem2  25536  dvfsum2  25543  deg1suble  25617  deg1mul3le  25626  plyeq0lem  25716  dgrcolem2  25780  geolim3  25844  aaliou3lem2  25848  aaliou3lem8  25850  ulmdvlem1  25904  radcnvlem1  25917  radcnvlem2  25918  dvradcnv  25925  pserulm  25926  pserdvlem2  25932  abelthlem2  25936  abelthlem5  25939  abelthlem7  25942  abelth2  25946  tangtx  26007  tanabsge  26008  tanord1  26038  argregt0  26110  argrege0  26111  argimgt0  26112  abslogle  26118  logcnlem4  26145  logtayllem  26159  abscxpbnd  26251  ang180lem2  26305  atanlogsublem  26410  atans2  26426  leibpi  26437  birthdaylem3  26448  cxplim  26466  cxp2limlem  26470  cxploglim2  26473  jensenlem2  26482  jensen  26483  amgmlem  26484  emcllem2  26491  emcllem4  26493  emcllem7  26496  zetacvg  26509  lgamgulmlem2  26524  lgamgulmlem5  26527  ftalem5  26571  basellem4  26578  basellem6  26580  basellem8  26582  basellem9  26583  chtwordi  26650  chpwordi  26651  ppiwordi  26656  ppiub  26697  vmalelog  26698  chtlepsi  26699  chtleppi  26703  chtublem  26704  chtub  26705  chpub  26713  logfaclbnd  26715  logfacrlim  26717  dchrptlem3  26759  bcmono  26770  bclbnd  26773  bposlem1  26777  bposlem6  26782  bposlem9  26785  lgsqrlem4  26842  2lgslem1c  26886  chebbnd1lem1  26962  chebbnd1lem3  26964  chebbnd1  26965  chtppilimlem1  26966  vmadivsum  26975  rplogsumlem2  26978  dchrisumlema  26981  dchrisumlem3  26984  dchrmusum2  26987  dchrvmasumlem3  26992  dchrvmasumiflem1  26994  dchrisum0flblem1  27001  dchrisum0re  27006  dchrisum0lem2a  27010  mulogsumlem  27024  mulog2sumlem1  27027  mulog2sumlem2  27028  2vmadivsumlem  27033  selberg2lem  27043  selberg3lem1  27050  selberg4lem1  27053  pntrlog2bndlem3  27072  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntpbnd1  27079  pntlemc  27088  pntlemr  27095  pntlemk  27099  pntlemo  27100  abvcxp  27108  ostth2lem1  27111  padicabv  27123  ostth2lem2  27127  ostth2lem3  27128  ostth2lem4  27129  ostth2  27130  noextendlt  27162  noextendgt  27163  nosupbnd1  27207  nosupbnd2lem1  27208  noinfbnd1  27222  noinfbnd2lem1  27223  lltropt  27357  addsproplem2  27444  addsproplem4  27446  addsproplem5  27447  addsproplem6  27448  mulsproplem5  27566  mulsproplem6  27567  mulsproplem7  27568  mulsproplem8  27569  slemuld  27584  mulsuniflem  27594  precsexlem9  27651  legso  27840  trgcopy  28045  eucrct2eupth  29488  nvmtri  29912  imsmetlem  29931  vacn  29935  nmcvcn  29936  smcnlem  29938  blometi  30044  ipblnfi  30096  minvecolem2  30116  hhssnv  30505  nmcoplbi  31269  nmopcoi  31336  nmopcoadji  31342  idleop  31372  cdj1i  31674  isoun  31911  xlt2addrd  31959  mgcf1o  32161  omndmul  32220  ogrpsub  32222  gsumle  32230  cycpmconjslem2  32302  archirngz  32323  ofldchr  32421  lssdimle  32681  fedgmullem2  32704  pstmxmet  32866  nexple  32996  esumpmono  33066  esumcvg  33073  meascnbl  33206  omsmon  33286  omsmeas  33311  dstfrvinc  33464  hgt750lemd  33649  hgt750lema  33658  hgt750leme  33659  swrdwlk  34106  derangenlem  34151  subfaclefac  34156  subfaclim  34168  erdszelem10  34180  sinccvglem  34646  iprodefisum  34700  gg-dvfsumlem2  35172  unbdqndv2lem2  35375  itg2gt0cn  36532  ibladdnclem  36533  iblabsnc  36541  iblmulc2nc  36542  itgabsnc  36546  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  mettrifi  36614  equivbnd2  36649  heiborlem6  36673  bfplem1  36679  bfp  36681  rrnmet  36686  rrndstprj1  36687  rrndstprj2  36688  dalawlem3  38733  dalawlem4  38734  dalawlem6  38736  dalawlem9  38739  dalawlem11  38741  dalawlem12  38742  dalawlem15  38745  cdleme3c  39090  cdleme7e  39107  cdleme26e  39219  cdleme26eALTN  39221  cdleme27a  39227  cdleme32c  39303  cdleme32e  39305  cdleme32le  39307  cdlemg9b  39493  cdlemg12b  39504  cdlemg12d  39506  trlcolem  39586  trlcone  39588  cdlemk7  39708  cdlemk7u  39730  cdlemk39  39776  cdlemk11ta  39789  cdlemk11tc  39805  mapdcnvatN  40526  factwoffsmonot  41012  frlmvscadiccat  41078  3cubeslem1  41408  irrapxlem5  41550  pell1qrge1  41594  pell1qrgaplem  41597  pell14qrgapw  41600  pellqrex  41603  pellfund14  41622  jm2.17a  41685  jm2.17c  41687  acongeq  41708  jm2.19  41718  jm2.27a  41730  jm2.27c  41732  jm3.1lem2  41743  areaquad  41951  rp-isfinite6  42255  hashnzfzclim  43067  binomcxplemnotnn0  43101  absimlere  44177  monoord2xrv  44181  ltmod  44341  dvbdfbdioolem2  44632  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  stoweidlem3  44706  stoweidlem26  44729  wallispilem1  44768  wallispilem5  44772  stirlinglem1  44777  stirlinglem5  44781  stirlinglem8  44784  stirlinglem10  44786  stirlinglem12  44788  fourierdlem6  44816  fourierdlem7  44817  fourierdlem14  44824  fourierdlem19  44829  fourierdlem35  44845  fourierdlem39  44849  fourierdlem42  44852  fourierdlem50  44859  fourierdlem73  44882  fourierdlem76  44885  fourierdlem77  44886  fourierdlem81  44890  fourierdlem90  44899  fourierdlem92  44901  fourierdlem93  44902  fourierdlem111  44920  fouriersw  44934  etransclem38  44975  sge0split  45112  ovnsslelem  45263  lighneallem4a  46263  rnghmsubcsetc  46829  rhmsubcsetc  46875  rhmsubcrngc  46881  rhmsubc  46942  rhmsubcALTV  46960  logbpw2m1  47207  dignn0flhalflem1  47255  dignn0flhalflem2  47256  1aryenef  47285  2aryenef  47296  2itscp  47421  amgmwlem  47803