Theorem 3brtr4d 5147

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

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  f1oiso2  7351  sucdom2  9186  ordtypelem6  9484  ttrcltr  9684  ttrclss  9688  ttrclselem2  9694  fin23lem26  10308  distrnq  10945  lediv12a  12107  recp1lt1  12112  ifle  13222  xleadd1a  13278  xlemul1a  13313  fldiv4p1lem1div2  13867  fldiv4lem1div2  13869  quoremz  13887  quoremnn0ALT  13889  intfracq  13891  modmulnn  13921  fzennn  14003  monoord2  14068  expgt1  14135  expmordi  14202  leexp2r  14209  leexp1a  14210  bernneq  14264  expmulnbnd  14270  digit1  14272  faclbnd  14325  faclbnd4lem3  14330  faclbnd4lem4  14331  faclbnd6  14334  facubnd  14335  hashdomi  14415  fzsdom2  14464  absrele  15358  absimle  15359  abstri  15381  abs2difabs  15385  limsupval2  15530  rlimrege0  15629  rlimrecl  15630  climsqz  15691  climsqz2  15692  rlimdiv  15696  rlimsqz  15700  rlimsqz2  15701  isercolllem1  15715  isercoll2  15719  fsumcvg2  15777  fsumrlim  15862  o1fsum  15864  cvgcmpce  15869  isumle  15897  climcndslem1  15902  climcndslem2  15903  harmonic  15912  expcnv  15917  explecnv  15918  geomulcvg  15929  efcllem  16130  ege2le3  16143  eflegeo  16176  rpnnen2lem4  16272  ruclem2  16287  ruclem8  16292  fsumdvds  16365  phibnd  16829  iserodd  16894  pcdvdstr  16935  pcprmpw2  16941  pockthg  16965  prmreclem4  16978  prmolefac  17105  2expltfac  17151  mod2ile  18549  pfxchn  18665  chnub  18677  chnccats1  18680  chnccat  18681  chnrev  18682  ex-chn2  18693  odsubdvds  19640  pgpfi  19674  fislw  19694  efgredlemd  19813  efgredlem  19816  frgpcpbl  19828  omndmul  20204  ogrpsub  20206  gsumle  20214  rnghmsubcsetc  20717  rhmsubcsetc  20746  rhmsubcrngc  20752  rhmsubc  20773  abvres  20911  abvtrivd  20912  znrrg  21683  ofldchr  21694  cstucnd  24408  psmetge0  24437  psmetres2  24439  xmetge0  24469  xmetres2  24486  imasf1oxmet  24500  comet  24638  stdbdxmet  24640  dscmet  24697  nrmmetd  24699  nmrtri  24749  tngngp  24779  nmolb2d  24843  nmoleub  24856  nmoco  24862  nmotri  24864  nmoid  24867  nmods  24869  cnmet  24896  xrsxmet  24935  metdstri  24977  metnrmlem3  24987  lebnumlem3  25090  ipcau2  25361  tcphcphlem1  25362  tcphcph  25364  trirn  25527  rrxmet  25535  rrxdstprj1  25536  minveclem2  25553  ovolunlem1a  25623  ovolscalem1  25640  volss  25660  voliunlem1  25677  volcn  25733  itg1climres  25841  mbfi1fseqlem5  25846  mbfi1fseqlem6  25847  itg2const2  25868  itg2seq  25869  itg2mulc  25874  itg2splitlem  25875  itg2monolem1  25877  itg2i1fseqle  25881  itg2i1fseq  25882  itg2i1fseq2  25883  itg2addlem  25885  itg2cnlem1  25888  itg2cnlem2  25889  iblss  25932  itgle  25937  ibladdlem  25947  iblabs  25956  iblabsr  25957  iblmulc2  25958  itgabs  25962  bddmulibl  25966  bddiblnc  25969  dvfsumabs  26150  dvfsumlem2  26154  dvfsum2  26161  deg1suble  26232  deg1mul3le  26242  plyeq0lem  26335  dgrcolem2  26399  geolim3  26468  aaliou3lem2  26472  aaliou3lem8  26474  ulmdvlem1  26528  radcnvlem1  26541  radcnvlem2  26542  dvradcnv  26549  pserulm  26550  pserdvlem2  26556  abelthlem2  26560  abelthlem5  26563  abelthlem7  26566  abelth2  26570  tangtx  26635  tanabsge  26636  tanord1  26667  argregt0  26740  argrege0  26741  argimgt0  26742  abslogle  26748  logcnlem4  26775  logtayllem  26789  abscxpbnd  26883  ang180lem2  26940  atanlogsublem  27045  atans2  27061  leibpi  27072  birthdaylem3  27083  cxplim  27101  cxp2limlem  27105  cxploglim2  27108  jensenlem2  27117  jensen  27118  amgmlem  27119  emcllem2  27126  emcllem4  27128  emcllem7  27131  zetacvg  27144  lgamgulmlem2  27159  lgamgulmlem5  27162  ftalem5  27206  basellem4  27213  basellem6  27215  basellem8  27217  basellem9  27218  chtwordi  27285  chpwordi  27286  ppiwordi  27291  ppiub  27333  vmalelog  27334  chtlepsi  27335  chtleppi  27339  chtublem  27340  chtub  27341  chpub  27349  logfaclbnd  27351  logfacrlim  27353  dchrptlem3  27395  bcmono  27406  bclbnd  27409  bposlem1  27413  bposlem6  27418  bposlem9  27421  lgsqrlem4  27478  2lgslem1c  27522  chebbnd1lem1  27598  chebbnd1lem3  27600  chebbnd1  27601  chtppilimlem1  27602  vmadivsum  27611  rplogsumlem2  27614  dchrisumlema  27617  dchrisumlem3  27620  dchrmusum2  27623  dchrvmasumlem3  27628  dchrvmasumiflem1  27630  dchrisum0flblem1  27637  dchrisum0re  27642  dchrisum0lem2a  27646  mulogsumlem  27660  mulog2sumlem1  27663  mulog2sumlem2  27664  2vmadivsumlem  27669  selberg2lem  27679  selberg3lem1  27686  selberg4lem1  27689  pntrlog2bndlem3  27708  pntrlog2bndlem5  27710  pntrlog2bndlem6  27712  pntpbnd1  27715  pntlemc  27724  pntlemr  27731  pntlemk  27735  pntlemo  27736  abvcxp  27744  ostth2lem1  27747  padicabv  27759  ostth2lem2  27763  ostth2lem3  27764  ostth2lem4  27765  ostth2  27766  noextendlt  27798  noextendgt  27799  nosupbnd1  27843  nosupbnd2lem1  27844  noinfbnd1  27858  noinfbnd2lem1  27859  lltr  28020  addsproplem2  28128  addsproplem4  28130  addsproplem5  28131  addsproplem6  28132  mulsproplem5  28278  mulsproplem6  28279  mulsproplem7  28280  mulsproplem8  28281  lemulsd  28296  mulsuniflem  28307  lemuls1ad  28340  precsexlem9  28373  bdaypw2n0bndlem  28621  legso  28833  trgcopy  29071  eucrct2eupth  30536  nvmtri  30963  imsmetlem  30982  vacn  30986  nmcvcn  30987  smcnlem  30989  blometi  31095  ipblnfi  31147  minvecolem2  31167  hhssnv  31556  nmcoplbi  32320  nmopcoi  32387  nmopcoadji  32393  idleop  32423  cdj1i  32725  isoun  32987  xlt2addrd  33044  nexple  33117  mgcf1o  33263  cycpmconjslem2  33415  archirngz  33449  elrgspnlem1  33502  q1pvsca  33838  lssdimle  33942  fedgmullem2  33964  fldextrspundglemul  34013  extdgfialglem1  34026  fldext2chn  34062  2sqr3minply  34114  cos9thpiminply  34122  pstmxmet  34231  esumpmono  34413  esumcvg  34420  meascnbl  34553  omsmon  34632  omsmeas  34657  dstfrvinc  34811  hgt750lemd  34979  hgt750lema  34988  hgt750leme  34989  swrdwlk  35517  derangenlem  35561  subfaclefac  35566  subfaclim  35578  erdszelem10  35590  sinccvglem  36062  iprodefisum  36131  unbdqndv2lem2  36987  itg2gt0cn  38213  ibladdnclem  38214  iblabsnc  38222  iblmulc2nc  38223  itgabsnc  38227  ftc1anclem7  38237  ftc1anclem8  38238  ftc1anc  38239  mettrifi  38295  equivbnd2  38330  heiborlem6  38354  bfplem1  38360  bfp  38362  rrnmet  38367  rrndstprj1  38368  rrndstprj2  38369  dalawlem3  40536  dalawlem4  40537  dalawlem6  40539  dalawlem9  40542  dalawlem11  40544  dalawlem12  40545  dalawlem15  40548  cdleme3c  40893  cdleme7e  40910  cdleme26e  41022  cdleme26eALTN  41024  cdleme27a  41030  cdleme32c  41106  cdleme32e  41108  cdleme32le  41110  cdlemg9b  41296  cdlemg12b  41307  cdlemg12d  41309  trlcolem  41389  trlcone  41391  cdlemk7  41511  cdlemk7u  41533  cdlemk39  41579  cdlemk11ta  41592  cdlemk11tc  41608  mapdcnvatN  42329  explt1d  42973  frlmvscadiccat  43169  3cubeslem1  43306  irrapxlem5  43444  pell1qrge1  43488  pell1qrgaplem  43491  pell14qrgapw  43494  pellqrex  43497  pellfund14  43516  jm2.17a  43578  jm2.17c  43580  acongeq  43601  jm2.19  43611  jm2.27a  43623  jm2.27c  43625  jm3.1lem2  43636  areaquad  43834  rp-isfinite6  44135  hashnzfzclim  44923  binomcxplemnotnn0  44957  absimlere  46084  monoord2xrv  46088  ltmod  46243  liminflelimsuplem  46380  dvbdfbdioolem2  46534  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  stoweidlem3  46608  stoweidlem26  46631  wallispilem1  46670  wallispilem5  46674  stirlinglem1  46679  stirlinglem5  46683  stirlinglem8  46686  stirlinglem10  46688  stirlinglem12  46690  fourierdlem6  46718  fourierdlem7  46719  fourierdlem14  46726  fourierdlem19  46731  fourierdlem35  46747  fourierdlem39  46751  fourierdlem42  46754  fourierdlem50  46761  fourierdlem73  46784  fourierdlem76  46787  fourierdlem77  46788  fourierdlem81  46792  fourierdlem90  46801  fourierdlem92  46803  fourierdlem93  46804  fourierdlem111  46822  fouriersw  46836  etransclem38  46877  sge0split  47014  ovnsslelem  47165  chnsubseq  47487  chnsuslle  47488  chnerlem1  47489  lighneallem4a  48248  rhmsubcALTV  48938  logbpw2m1  49231  dignn0flhalflem1  49279  dignn0flhalflem2  49280  1aryenef  49309  2aryenef  49320  2itscp  49445  amgmwlem  50475