MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3brtr4d Structured version   Visualization version   Unicode version

Theorem 3brtr4d 4449
Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)
Hypotheses
Ref Expression
3brtr4d.1  |-  ( ph  ->  A R B )
3brtr4d.2  |-  ( ph  ->  C  =  A )
3brtr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3brtr4d  |-  ( ph  ->  C R D )

Proof of Theorem 3brtr4d
StepHypRef Expression
1 3brtr4d.1 . 2  |-  ( ph  ->  A R B )
2 3brtr4d.2 . . 3  |-  ( ph  ->  C  =  A )
3 3brtr4d.3 . . 3  |-  ( ph  ->  D  =  B )
42, 3breq12d 4431 . 2  |-  ( ph  ->  ( C R D  <-> 
A R B ) )
51, 4mpbird 240 1  |-  ( ph  ->  C R D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455   class class class wbr 4418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4419
This theorem is referenced by:  f1oiso2  6273  sucdom2  7799  ordtypelem6  8069  cdaen  8634  cdacomen  8642  cdadom1  8647  fin23lem26  8786  distrnq  9417  lediv12a  10532  recp1lt1  10537  ifle  11524  xleadd1a  11573  xlemul1a  11608  quoremz  12120  quoremnn0ALT  12122  intfracq  12124  modmulnn  12152  fzennn  12219  monoord2  12282  expgt1  12348  leexp2r  12368  leexp1a  12369  bernneq  12436  expmulnbnd  12442  digit1  12444  faclbnd  12513  faclbnd4lem3  12518  faclbnd4lem4  12519  faclbnd6  12522  facubnd  12523  hashdomi  12597  fzsdom2  12639  absrele  13426  absimle  13427  abstri  13448  abs2difabs  13452  limsupval2  13595  limsupval2OLD  13596  rlimrege0  13698  rlimrecl  13699  climsqz  13759  climsqz2  13760  rlimdiv  13764  rlimsqz  13768  rlimsqz2  13769  isercolllem1  13783  isercoll2  13787  fsumcvg2  13848  fsumrlim  13926  o1fsum  13928  cvgcmpce  13933  isumle  13957  climcndslem1  13962  climcndslem2  13963  harmonic  13972  expcnv  13977  explecnv  13978  geomulcvg  13987  efcllem  14187  ege2le3  14199  eflegeo  14230  rpnnen2lem4  14325  ruclem2  14339  ruclem8  14344  fsumdvds  14403  phibnd  14774  iserodd  14840  pcdvdstr  14880  pcprmpw2  14886  pockthg  14905  prmreclem4  14918  prmolefac  15059  prmorlefacOLD  15073  prmordvdslcmsOLDOLD  15076  2expltfac  15118  mod2ile  16407  odsubdvds  17275  pgpfi  17312  fislw  17332  efgredlemd  17449  efgredlem  17452  frgpcpbl  17464  abvres  18122  abvtrivd  18123  znrrg  19191  cstucnd  21354  psmetge0  21383  psmetres2  21385  xmetge0  21414  xmetres2  21431  imasf1oxmet  21445  comet  21583  stdbdxmet  21585  dscmet  21642  nrmmetd  21644  nmrtri  21692  tngngp  21717  nmolb2d  21778  nmoleub  21791  nmoleubOLD  21807  nmoco  21813  nmotri  21815  nmoid  21818  nmods  21820  cnmet  21847  xrsxmet  21882  metdstri  21923  metnrmlem3  21933  metdstriOLD  21938  metnrmlem3OLD  21948  lebnumlem3  22046  lebnumlem3OLD  22049  ipcau2  22263  tchcphlem1  22264  tchcph  22266  trirn  22409  rrxmet  22417  rrxdstprj1  22418  minveclem2  22423  minveclem2OLD  22435  ovolunlem1a  22504  ovolscalem1  22521  volss  22542  voliunlem1  22559  volcn  22620  itg1climres  22728  mbfi1fseqlem5  22733  mbfi1fseqlem6  22734  itg2const2  22755  itg2seq  22756  itg2mulc  22761  itg2splitlem  22762  itg2monolem1  22764  itg2i1fseqle  22768  itg2i1fseq  22769  itg2i1fseq2  22770  itg2addlem  22772  itg2cnlem1  22775  itg2cnlem2  22776  iblss  22818  itgle  22823  ibladdlem  22833  iblabs  22842  iblabsr  22843  iblmulc2  22844  itgabs  22848  bddmulibl  22852  dvfsumabs  23031  dvfsumlem2  23035  dvfsum2  23042  deg1suble  23112  deg1mul3le  23121  plyeq0lem  23220  dgrcolem2  23284  geolim3  23351  aaliou3lem2  23355  aaliou3lem8  23357  ulmdvlem1  23411  radcnvlem1  23424  radcnvlem2  23425  dvradcnv  23432  pserulm  23433  pserdvlem2  23439  abelthlem2  23443  abelthlem5  23446  abelthlem7  23449  abelth2  23453  tangtx  23516  tanabsge  23517  tanord1  23542  argregt0  23615  argrege0  23616  argimgt0  23617  abslogle  23623  logcnlem4  23646  logtayllem  23660  abscxpbnd  23749  ang180lem2  23795  atanlogsublem  23897  atans2  23913  leibpi  23924  birthdaylem3  23935  cxplim  23953  cxp2limlem  23957  cxploglim2  23960  jensenlem2  23969  jensen  23970  amgmlem  23971  emcllem2  23978  emcllem4  23980  emcllem7  23983  zetacvg  23996  lgamgulmlem2  24011  lgamgulmlem5  24014  lgamcvg2  24036  ftalem5  24057  ftalem5OLD  24059  basellem4  24066  basellem6  24068  basellem8  24070  basellem9  24071  chtwordi  24139  chpwordi  24140  ppiwordi  24145  ppiub  24188  vmalelog  24189  chtlepsi  24190  chtleppi  24194  chtublem  24195  chtub  24196  chpub  24204  logfaclbnd  24206  logfacrlim  24208  dchrptlem3  24250  bcmono  24261  bclbnd  24264  bposlem1  24268  bposlem6  24273  bposlem9  24276  lgsqrlem4  24328  chebbnd1lem1  24363  chebbnd1lem3  24365  chebbnd1  24366  chtppilimlem1  24367  vmadivsum  24376  rplogsumlem2  24379  dchrisumlema  24382  dchrisumlem3  24385  dchrmusum2  24388  dchrvmasumlem3  24393  dchrvmasumiflem1  24395  dchrisum0flblem1  24402  dchrisum0re  24407  dchrisum0lem2a  24411  mulogsumlem  24425  mulog2sumlem1  24428  mulog2sumlem2  24429  2vmadivsumlem  24434  selberg2lem  24444  selberg3lem1  24451  selberg4lem1  24454  pntrlog2bndlem3  24473  pntrlog2bndlem5  24475  pntrlog2bndlem6  24477  pntpbnd1  24480  pntlemc  24489  pntlemr  24496  pntlemk  24500  pntlemo  24501  abvcxp  24509  ostth2lem1  24512  padicabv  24524  ostth2lem2  24528  ostth2lem3  24529  ostth2lem4  24530  ostth2  24531  legso  24700  trgcopy  24902  nvmtri  26356  imsmetlem  26378  vacn  26386  nmcvcn  26387  smcnlem  26389  blometi  26500  ipblnfi  26553  minvecolem2  26573  minvecolem2OLD  26583  hhssnv  26971  nmcoplbi  27737  nmopcoi  27804  nmopcoadji  27810  idleop  27840  cdj1i  28142  isoun  28334  xlt2addrd  28390  omndmul  28528  ogrpsub  28531  archirngz  28557  gsumle  28593  ofldchr  28628  pstmxmet  28751  nexple  28882  esumpmono  28951  esumcvg  28958  meascnbl  29092  omsmon  29176  omsmonOLD  29180  omsmeas  29205  omsmeasOLD  29206  dstfrvinc  29359  derangenlem  29944  subfaclefac  29949  subfaclim  29961  erdszelem10  29973  sinccvglem  30366  iprodefisum  30427  itg2gt0cn  32043  ibladdnclem  32044  iblabsnc  32052  iblmulc2nc  32053  itgabsnc  32057  bddiblnc  32058  ftc1anclem7  32069  ftc1anclem8  32070  ftc1anc  32071  mettrifi  32132  equivbnd2  32170  heiborlem6  32194  bfplem1  32200  bfp  32202  rrnmet  32207  rrndstprj1  32208  rrndstprj2  32209  dalawlem3  33484  dalawlem4  33485  dalawlem6  33487  dalawlem9  33490  dalawlem11  33492  dalawlem12  33493  dalawlem15  33496  cdleme3c  33842  cdleme7e  33859  cdleme26e  33972  cdleme26eALTN  33974  cdleme27a  33980  cdleme32c  34056  cdleme32e  34058  cdleme32le  34060  cdlemg9b  34246  cdlemg12b  34257  cdlemg12d  34259  trlcolem  34339  trlcone  34341  cdlemk7  34461  cdlemk7u  34483  cdlemk39  34529  cdlemk11ta  34542  cdlemk11tc  34558  mapdcnvatN  35280  irrapxlem5  35716  pell1qrge1  35762  pell1qrgaplem  35765  pell14qrgapw  35768  pellqrex  35772  pellfund14  35792  expmordi  35841  jm2.17a  35856  jm2.17c  35858  acongeq  35879  jm2.19  35894  jm2.27a  35906  jm2.27c  35908  jm3.1lem2  35919  areaquad  36147  rp-isfinite6  36209  hashnzfzclim  36716  binomcxplemnotnn0  36750  ltmod  37804  dvbdfbdioolem2  37887  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  stoweidlem3  37964  stoweidlem26  37987  wallispilem1  38028  wallispilem5  38032  stirlinglem1  38037  stirlinglem5  38041  stirlinglem8  38044  stirlinglem10  38046  stirlinglem12  38048  fourierdlem6  38076  fourierdlem7  38077  fourierdlem14  38084  fourierdlem19  38089  fourierdlem35  38106  fourierdlem39  38110  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem50  38121  fourierdlem73  38144  fourierdlem76  38147  fourierdlem77  38148  fourierdlem81  38152  fourierdlem90  38161  fourierdlem92  38163  fourierdlem93  38164  fourierdlem111  38182  fouriersw  38196  etransclem38  38238  sge0split  38354  rnghmsubcsetc  40348  rhmsubcsetc  40394  rhmsubcrngc  40400  rhmsubc  40461  rhmsubcALTV  40480  logbpw2m1  40747  dignn0flhalflem1  40795  dignn0flhalflem2  40796
  Copyright terms: Public domain W3C validator