Theorem 3brtr4d 5174

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

Syntax hints:   → wi 4   = wceq 1534   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143

This theorem is referenced by:  f1oiso2  7354  sucdom2OLD  9100  sucdom2  9224  ordtypelem6  9540  ttrcltr  9733  ttrclss  9737  ttrclselem2  9743  fin23lem26  10342  distrnq  10978  lediv12a  12131  recp1lt1  12136  ifle  13202  xleadd1a  13258  xlemul1a  13293  fldiv4p1lem1div2  13826  fldiv4lem1div2  13828  quoremz  13846  quoremnn0ALT  13848  intfracq  13850  modmulnn  13880  fzennn  13959  monoord2  14024  expgt1  14091  expmordi  14157  leexp2r  14164  leexp1a  14165  bernneq  14217  expmulnbnd  14223  digit1  14225  faclbnd  14275  faclbnd4lem3  14280  faclbnd4lem4  14281  faclbnd6  14284  facubnd  14285  hashdomi  14365  fzsdom2  14413  absrele  15281  absimle  15282  abstri  15303  abs2difabs  15307  limsupval2  15450  rlimrege0  15549  rlimrecl  15550  climsqz  15611  climsqz2  15612  rlimdiv  15618  rlimsqz  15622  rlimsqz2  15623  isercolllem1  15637  isercoll2  15641  fsumcvg2  15699  fsumrlim  15783  o1fsum  15785  cvgcmpce  15790  isumle  15816  climcndslem1  15821  climcndslem2  15822  harmonic  15831  expcnv  15836  explecnv  15837  geomulcvg  15848  efcllem  16047  ege2le3  16060  eflegeo  16091  rpnnen2lem4  16187  ruclem2  16202  ruclem8  16207  fsumdvds  16278  phibnd  16733  iserodd  16797  pcdvdstr  16838  pcprmpw2  16844  pockthg  16868  prmreclem4  16881  prmolefac  17008  2expltfac  17055  mod2ile  18479  odsubdvds  19519  pgpfi  19553  fislw  19573  efgredlemd  19692  efgredlem  19695  frgpcpbl  19707  rnghmsubcsetc  20559  rhmsubcsetc  20588  rhmsubcrngc  20594  rhmsubc  20615  abvres  20712  abvtrivd  20713  znrrg  21492  cstucnd  24182  psmetge0  24211  psmetres2  24213  xmetge0  24243  xmetres2  24260  imasf1oxmet  24274  comet  24415  stdbdxmet  24417  dscmet  24474  nrmmetd  24476  nmrtri  24526  tngngp  24564  nmolb2d  24628  nmoleub  24641  nmoco  24647  nmotri  24649  nmoid  24652  nmods  24654  cnmet  24681  xrsxmet  24718  metdstri  24760  metnrmlem3  24770  lebnumlem3  24882  ipcau2  25155  tcphcphlem1  25156  tcphcph  25158  trirn  25321  rrxmet  25329  rrxdstprj1  25330  minveclem2  25347  ovolunlem1a  25418  ovolscalem1  25435  volss  25455  voliunlem1  25472  volcn  25528  itg1climres  25637  mbfi1fseqlem5  25642  mbfi1fseqlem6  25643  itg2const2  25664  itg2seq  25665  itg2mulc  25670  itg2splitlem  25671  itg2monolem1  25673  itg2i1fseqle  25677  itg2i1fseq  25678  itg2i1fseq2  25679  itg2addlem  25681  itg2cnlem1  25684  itg2cnlem2  25685  iblss  25727  itgle  25732  ibladdlem  25742  iblabs  25751  iblabsr  25752  iblmulc2  25753  itgabs  25757  bddmulibl  25761  bddiblnc  25764  dvfsumabs  25950  dvfsumlem2  25954  dvfsumlem2OLD  25955  dvfsum2  25962  deg1suble  26036  deg1mul3le  26045  plyeq0lem  26137  dgrcolem2  26202  geolim3  26267  aaliou3lem2  26271  aaliou3lem8  26273  ulmdvlem1  26329  radcnvlem1  26342  radcnvlem2  26343  dvradcnv  26350  pserulm  26351  pserdvlem2  26358  abelthlem2  26362  abelthlem5  26365  abelthlem7  26368  abelth2  26372  tangtx  26433  tanabsge  26434  tanord1  26464  argregt0  26537  argrege0  26538  argimgt0  26539  abslogle  26545  logcnlem4  26572  logtayllem  26586  abscxpbnd  26681  ang180lem2  26735  atanlogsublem  26840  atans2  26856  leibpi  26867  birthdaylem3  26878  cxplim  26897  cxp2limlem  26901  cxploglim2  26904  jensenlem2  26913  jensen  26914  amgmlem  26915  emcllem2  26922  emcllem4  26924  emcllem7  26927  zetacvg  26940  lgamgulmlem2  26955  lgamgulmlem5  26958  ftalem5  27002  basellem4  27009  basellem6  27011  basellem8  27013  basellem9  27014  chtwordi  27081  chpwordi  27082  ppiwordi  27087  ppiub  27130  vmalelog  27131  chtlepsi  27132  chtleppi  27136  chtublem  27137  chtub  27138  chpub  27146  logfaclbnd  27148  logfacrlim  27150  dchrptlem3  27192  bcmono  27203  bclbnd  27206  bposlem1  27210  bposlem6  27215  bposlem9  27218  lgsqrlem4  27275  2lgslem1c  27319  chebbnd1lem1  27395  chebbnd1lem3  27397  chebbnd1  27398  chtppilimlem1  27399  vmadivsum  27408  rplogsumlem2  27411  dchrisumlema  27414  dchrisumlem3  27417  dchrmusum2  27420  dchrvmasumlem3  27425  dchrvmasumiflem1  27427  dchrisum0flblem1  27434  dchrisum0re  27439  dchrisum0lem2a  27443  mulogsumlem  27457  mulog2sumlem1  27460  mulog2sumlem2  27461  2vmadivsumlem  27466  selberg2lem  27476  selberg3lem1  27483  selberg4lem1  27486  pntrlog2bndlem3  27505  pntrlog2bndlem5  27507  pntrlog2bndlem6  27509  pntpbnd1  27512  pntlemc  27521  pntlemr  27528  pntlemk  27532  pntlemo  27533  abvcxp  27541  ostth2lem1  27544  padicabv  27556  ostth2lem2  27560  ostth2lem3  27561  ostth2lem4  27562  ostth2  27563  noextendlt  27595  noextendgt  27596  nosupbnd1  27640  nosupbnd2lem1  27641  noinfbnd1  27655  noinfbnd2lem1  27656  lltropt  27792  addsproplem2  27880  addsproplem4  27882  addsproplem5  27883  addsproplem6  27884  mulsproplem5  28013  mulsproplem6  28014  mulsproplem7  28015  mulsproplem8  28016  slemuld  28031  mulsuniflem  28042  slemul1ad  28075  precsexlem9  28106  legso  28396  trgcopy  28601  eucrct2eupth  30048  nvmtri  30474  imsmetlem  30493  vacn  30497  nmcvcn  30498  smcnlem  30500  blometi  30606  ipblnfi  30658  minvecolem2  30678  hhssnv  31067  nmcoplbi  31831  nmopcoi  31898  nmopcoadji  31904  idleop  31934  cdj1i  32236  isoun  32475  xlt2addrd  32522  mgcf1o  32724  omndmul  32788  ogrpsub  32790  gsumle  32798  cycpmconjslem2  32870  archirngz  32891  ofldchr  33023  q1pvsca  33260  lssdimle  33291  fedgmullem2  33314  pstmxmet  33488  nexple  33618  esumpmono  33688  esumcvg  33695  meascnbl  33828  omsmon  33908  omsmeas  33933  dstfrvinc  34086  hgt750lemd  34270  hgt750lema  34279  hgt750leme  34280  swrdwlk  34726  derangenlem  34771  subfaclefac  34776  subfaclim  34788  erdszelem10  34800  sinccvglem  35266  iprodefisum  35325  unbdqndv2lem2  35975  itg2gt0cn  37137  ibladdnclem  37138  iblabsnc  37146  iblmulc2nc  37147  itgabsnc  37151  ftc1anclem7  37161  ftc1anclem8  37162  ftc1anc  37163  mettrifi  37219  equivbnd2  37254  heiborlem6  37278  bfplem1  37284  bfp  37286  rrnmet  37291  rrndstprj1  37292  rrndstprj2  37293  dalawlem3  39335  dalawlem4  39336  dalawlem6  39338  dalawlem9  39341  dalawlem11  39343  dalawlem12  39344  dalawlem15  39347  cdleme3c  39692  cdleme7e  39709  cdleme26e  39821  cdleme26eALTN  39823  cdleme27a  39829  cdleme32c  39905  cdleme32e  39907  cdleme32le  39909  cdlemg9b  40095  cdlemg12b  40106  cdlemg12d  40108  trlcolem  40188  trlcone  40190  cdlemk7  40310  cdlemk7u  40332  cdlemk39  40378  cdlemk11ta  40391  cdlemk11tc  40407  mapdcnvatN  41128  factwoffsmonot  41666  frlmvscadiccat  41718  3cubeslem1  42076  irrapxlem5  42218  pell1qrge1  42262  pell1qrgaplem  42265  pell14qrgapw  42268  pellqrex  42271  pellfund14  42290  jm2.17a  42353  jm2.17c  42355  acongeq  42376  jm2.19  42386  jm2.27a  42398  jm2.27c  42400  jm3.1lem2  42411  areaquad  42616  rp-isfinite6  42920  hashnzfzclim  43731  binomcxplemnotnn0  43765  absimlere  44834  monoord2xrv  44838  ltmod  44998  dvbdfbdioolem2  45289  ioodvbdlimc1lem2  45292  ioodvbdlimc2lem  45294  stoweidlem3  45363  stoweidlem26  45386  wallispilem1  45425  wallispilem5  45429  stirlinglem1  45434  stirlinglem5  45438  stirlinglem8  45441  stirlinglem10  45443  stirlinglem12  45445  fourierdlem6  45473  fourierdlem7  45474  fourierdlem14  45481  fourierdlem19  45486  fourierdlem35  45502  fourierdlem39  45506  fourierdlem42  45509  fourierdlem50  45516  fourierdlem73  45539  fourierdlem76  45542  fourierdlem77  45543  fourierdlem81  45547  fourierdlem90  45556  fourierdlem92  45558  fourierdlem93  45559  fourierdlem111  45577  fouriersw  45591  etransclem38  45632  sge0split  45769  ovnsslelem  45920  lighneallem4a  46920  rhmsubcALTV  47319  logbpw2m1  47612  dignn0flhalflem1  47660  dignn0flhalflem2  47661  1aryenef  47690  2aryenef  47701  2itscp  47826  amgmwlem  48207