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

Theorem 3brtr4d 4454
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 4436 . 2  |-  ( ph  ->  ( C R D  <-> 
A R B ) )
51, 4mpbird 235 1  |-  ( ph  ->  C R D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   class class class wbr 4423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424
This theorem is referenced by:  f1oiso2  6258  sucdom2  7777  ordtypelem6  8047  cdaen  8610  cdacomen  8618  cdadom1  8623  fin23lem26  8762  distrnq  9393  lediv12a  10506  recp1lt1  10511  ifle  11497  xleadd1a  11546  xlemul1a  11581  quoremz  12088  quoremnn0ALT  12090  intfracq  12092  modmulnn  12120  fzennn  12187  monoord2  12250  expgt1  12316  leexp2r  12336  leexp1a  12337  bernneq  12404  expmulnbnd  12410  digit1  12412  faclbnd  12481  faclbnd4lem3  12486  faclbnd4lem4  12487  faclbnd6  12490  facubnd  12491  hashdomi  12565  fzsdom2  12604  absrele  13371  absimle  13372  abstri  13393  abs2difabs  13397  limsupval2  13539  limsupval2OLD  13540  rlimrege0  13642  rlimrecl  13643  climsqz  13703  climsqz2  13704  rlimdiv  13708  rlimsqz  13712  rlimsqz2  13713  isercolllem1  13727  isercoll2  13731  fsumcvg2  13792  fsumrlim  13870  o1fsum  13872  cvgcmpce  13877  isumle  13901  climcndslem1  13906  climcndslem2  13907  harmonic  13916  expcnv  13921  explecnv  13922  geomulcvg  13931  efcllem  14131  ege2le3  14143  eflegeo  14174  rpnnen2lem4  14269  ruclem2  14283  ruclem8  14288  fsumdvds  14347  phibnd  14718  iserodd  14784  pcdvdstr  14824  pcprmpw2  14830  pockthg  14849  prmreclem4  14862  prmolefac  15003  prmorlefacOLD  15017  prmordvdslcmsOLDOLD  15020  2expltfac  15062  mod2ile  16351  odsubdvds  17219  pgpfi  17256  fislw  17276  efgredlemd  17393  efgredlem  17396  frgpcpbl  17408  abvres  18066  abvtrivd  18067  znrrg  19134  cstucnd  21297  psmetge0  21326  psmetres2  21328  xmetge0  21357  xmetres2  21374  imasf1oxmet  21388  comet  21526  stdbdxmet  21528  dscmet  21585  nrmmetd  21587  nmrtri  21635  tngngp  21660  nmolb2d  21721  nmoleub  21734  nmoleubOLD  21750  nmoco  21756  nmotri  21758  nmoid  21761  nmods  21763  cnmet  21790  xrsxmet  21825  metdstri  21866  metnrmlem3  21876  metdstriOLD  21881  metnrmlem3OLD  21891  lebnumlem3  21989  lebnumlem3OLD  21992  ipcau2  22206  tchcphlem1  22207  tchcph  22209  trirn  22352  rrxmet  22360  rrxdstprj1  22361  minveclem2  22366  minveclem2OLD  22378  ovolunlem1a  22447  ovolscalem1  22464  volss  22485  voliunlem1  22501  volcn  22562  itg1climres  22670  mbfi1fseqlem5  22675  mbfi1fseqlem6  22676  itg2const2  22697  itg2seq  22698  itg2mulc  22703  itg2splitlem  22704  itg2monolem1  22706  itg2i1fseqle  22710  itg2i1fseq  22711  itg2i1fseq2  22712  itg2addlem  22714  itg2cnlem1  22717  itg2cnlem2  22718  iblss  22760  itgle  22765  ibladdlem  22775  iblabs  22784  iblabsr  22785  iblmulc2  22786  itgabs  22790  bddmulibl  22794  dvfsumabs  22973  dvfsumlem2  22977  dvfsum2  22984  deg1suble  23054  deg1mul3le  23063  plyeq0lem  23162  dgrcolem2  23226  geolim3  23293  aaliou3lem2  23297  aaliou3lem8  23299  ulmdvlem1  23353  radcnvlem1  23366  radcnvlem2  23367  dvradcnv  23374  pserulm  23375  pserdvlem2  23381  abelthlem2  23385  abelthlem5  23388  abelthlem7  23391  abelth2  23395  tangtx  23458  tanabsge  23459  tanord1  23484  argregt0  23557  argrege0  23558  argimgt0  23559  abslogle  23565  logcnlem4  23588  logtayllem  23602  abscxpbnd  23691  ang180lem2  23737  atanlogsublem  23839  atans2  23855  leibpi  23866  birthdaylem3  23877  cxplim  23895  cxp2limlem  23899  cxploglim2  23902  jensenlem2  23911  jensen  23912  amgmlem  23913  emcllem2  23920  emcllem4  23922  emcllem7  23925  zetacvg  23938  lgamgulmlem2  23953  lgamgulmlem5  23956  lgamcvg2  23978  ftalem5  23999  ftalem5OLD  24001  basellem4  24008  basellem6  24010  basellem8  24012  basellem9  24013  chtwordi  24081  chpwordi  24082  ppiwordi  24087  ppiub  24130  vmalelog  24131  chtlepsi  24132  chtleppi  24136  chtublem  24137  chtub  24138  chpub  24146  logfaclbnd  24148  logfacrlim  24150  dchrptlem3  24192  bcmono  24203  bclbnd  24206  bposlem1  24210  bposlem6  24215  bposlem9  24218  lgsqrlem4  24270  chebbnd1lem1  24305  chebbnd1lem3  24307  chebbnd1  24308  chtppilimlem1  24309  vmadivsum  24318  rplogsumlem2  24321  dchrisumlema  24324  dchrisumlem3  24327  dchrmusum2  24330  dchrvmasumlem3  24335  dchrvmasumiflem1  24337  dchrisum0flblem1  24344  dchrisum0re  24349  dchrisum0lem2a  24353  mulogsumlem  24367  mulog2sumlem1  24370  mulog2sumlem2  24371  2vmadivsumlem  24376  selberg2lem  24386  selberg3lem1  24393  selberg4lem1  24396  pntrlog2bndlem3  24415  pntrlog2bndlem5  24417  pntrlog2bndlem6  24419  pntpbnd1  24422  pntlemc  24431  pntlemr  24438  pntlemk  24442  pntlemo  24443  abvcxp  24451  ostth2lem1  24454  padicabv  24466  ostth2lem2  24470  ostth2lem3  24471  ostth2lem4  24472  ostth2  24473  legso  24642  trgcopy  24844  nvmtri  26298  imsmetlem  26320  vacn  26328  nmcvcn  26329  smcnlem  26331  blometi  26442  ipblnfi  26495  minvecolem2  26515  minvecolem2OLD  26525  hhssnv  26913  nmcoplbi  27679  nmopcoi  27746  nmopcoadji  27752  idleop  27782  cdj1i  28084  isoun  28284  xlt2addrd  28344  omndmul  28484  ogrpsub  28487  archirngz  28513  gsumle  28549  ofldchr  28585  pstmxmet  28708  nexple  28839  esumpmono  28908  esumcvg  28915  meascnbl  29049  omsmon  29134  omsmonOLD  29138  omsmeas  29163  omsmeasOLD  29164  dstfrvinc  29317  derangenlem  29902  subfaclefac  29907  subfaclim  29919  erdszelem10  29931  sinccvglem  30324  iprodefisum  30384  itg2gt0cn  31961  ibladdnclem  31962  iblabsnc  31970  iblmulc2nc  31971  itgabsnc  31975  bddiblnc  31976  ftc1anclem7  31987  ftc1anclem8  31988  ftc1anc  31989  mettrifi  32050  equivbnd2  32088  heiborlem6  32112  bfplem1  32118  bfp  32120  rrnmet  32125  rrndstprj1  32126  rrndstprj2  32127  dalawlem3  33407  dalawlem4  33408  dalawlem6  33410  dalawlem9  33413  dalawlem11  33415  dalawlem12  33416  dalawlem15  33419  cdleme3c  33765  cdleme7e  33782  cdleme26e  33895  cdleme26eALTN  33897  cdleme27a  33903  cdleme32c  33979  cdleme32e  33981  cdleme32le  33983  cdlemg9b  34169  cdlemg12b  34180  cdlemg12d  34182  trlcolem  34262  trlcone  34264  cdlemk7  34384  cdlemk7u  34406  cdlemk39  34452  cdlemk11ta  34465  cdlemk11tc  34481  mapdcnvatN  35203  irrapxlem5  35640  pell1qrge1  35686  pell1qrgaplem  35689  pell14qrgapw  35692  pellqrex  35696  pellfund14  35716  expmordi  35765  jm2.17a  35780  jm2.17c  35782  acongeq  35803  jm2.19  35818  jm2.27a  35830  jm2.27c  35832  jm3.1lem2  35843  areaquad  36071  rp-isfinite6  36133  hashnzfzclim  36641  binomcxplemnotnn0  36675  ltmod  37658  dvbdfbdioolem2  37741  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  stoweidlem3  37803  stoweidlem26  37826  wallispilem1  37867  wallispilem5  37871  stirlinglem1  37876  stirlinglem5  37880  stirlinglem8  37883  stirlinglem10  37885  stirlinglem12  37887  fourierdlem6  37915  fourierdlem7  37916  fourierdlem14  37923  fourierdlem19  37928  fourierdlem35  37945  fourierdlem39  37949  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem50  37960  fourierdlem73  37983  fourierdlem76  37986  fourierdlem77  37987  fourierdlem81  37991  fourierdlem90  38000  fourierdlem92  38002  fourierdlem93  38003  fourierdlem111  38021  fouriersw  38035  etransclem38  38077  sge0split  38159  rnghmsubcsetc  39599  rhmsubcsetc  39645  rhmsubcrngc  39651  rhmsubc  39712  rhmsubcALTV  39731  logbpw2m1  40000  dignn0flhalflem1  40048  dignn0flhalflem2  40049
  Copyright terms: Public domain W3C validator