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

Theorem 3brtr4d 4467
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 4450 . 2  |-  ( ph  ->  ( C R D  <-> 
A R B ) )
51, 4mpbird 232 1  |-  ( ph  ->  C R D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   class class class wbr 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438
This theorem is referenced by:  f1oiso2  6233  sucdom2  7716  ordtypelem6  7951  cdaen  8556  cdacomen  8564  cdadom1  8569  fin23lem26  8708  distrnq  9342  lediv12a  10445  recp1lt1  10450  ifle  11407  xleadd1a  11456  xlemul1a  11491  quoremz  11964  quoremnn0ALT  11966  intfracq  11968  modmulnn  11995  fzennn  12060  monoord2  12120  expgt1  12186  leexp2r  12205  leexp1a  12206  bernneq  12274  expmulnbnd  12280  digit1  12282  faclbnd  12350  faclbnd4lem3  12355  faclbnd4lem4  12356  faclbnd6  12359  facubnd  12360  hashdomi  12430  fzsdom2  12468  absrele  13123  absimle  13124  abstri  13145  abs2difabs  13149  limsupval2  13285  rlimrege0  13384  rlimrecl  13385  climsqz  13445  climsqz2  13446  rlimdiv  13450  rlimsqz  13454  rlimsqz2  13455  isercolllem1  13469  isercoll2  13473  fsumcvg2  13531  fsumrlim  13607  o1fsum  13609  cvgcmpce  13614  isumle  13638  climcndslem1  13643  climcndslem2  13644  harmonic  13652  expcnv  13657  explecnv  13658  geomulcvg  13667  efcllem  13795  ege2le3  13807  eflegeo  13838  rpnnen2lem4  13933  ruclem2  13947  ruclem8  13952  fsumdvds  14011  phibnd  14283  iserodd  14341  pcdvdstr  14381  pcprmpw2  14387  pockthg  14406  prmreclem4  14419  2expltfac  14559  mod2ile  15715  odsubdvds  16570  pgpfi  16604  fislw  16624  efgredlemd  16741  efgredlem  16744  frgpcpbl  16756  abvres  17467  abvtrivd  17468  znrrg  18582  cstucnd  20765  psmetge0  20794  psmetres2  20796  xmetge0  20825  xmetres2  20842  imasf1oxmet  20856  comet  20994  stdbdxmet  20996  dscmet  21071  nrmmetd  21073  nmrtri  21121  tngngp  21146  nmolb2d  21203  nmoleub  21216  nmoco  21222  nmotri  21224  nmoid  21227  nmods  21229  cnmet  21257  xrsxmet  21292  metdstri  21333  metnrmlem3  21343  lebnumlem3  21441  ipcau2  21655  tchcphlem1  21656  tchcph  21658  trirn  21805  rrxmet  21813  rrxdstprj1  21814  minveclem2  21819  ovolunlem1a  21885  ovolscalem1  21902  volss  21922  voliunlem1  21938  volcn  21993  itg1climres  22099  mbfi1fseqlem5  22104  mbfi1fseqlem6  22105  itg2const2  22126  itg2seq  22127  itg2mulc  22132  itg2splitlem  22133  itg2monolem1  22135  itg2i1fseqle  22139  itg2i1fseq  22140  itg2i1fseq2  22141  itg2addlem  22143  itg2cnlem1  22146  itg2cnlem2  22147  iblss  22189  itgle  22194  ibladdlem  22204  iblabs  22213  iblabsr  22214  iblmulc2  22215  itgabs  22219  bddmulibl  22223  dvfsumabs  22402  dvfsumlem2  22406  dvfsum2  22413  deg1suble  22486  deg1mul3le  22495  plyeq0lem  22585  dgrcolem2  22649  geolim3  22713  aaliou3lem2  22717  aaliou3lem8  22719  ulmdvlem1  22773  radcnvlem1  22786  radcnvlem2  22787  dvradcnv  22794  pserulm  22795  pserdvlem2  22801  abelthlem2  22805  abelthlem5  22808  abelthlem7  22811  abelth2  22815  tangtx  22876  tanabsge  22877  tanord1  22902  argregt0  22973  argrege0  22974  argimgt0  22975  abslogle  22981  logcnlem4  23004  logtayllem  23018  abscxpbnd  23105  ang180lem2  23120  atanlogsublem  23224  atans2  23240  leibpi  23251  birthdaylem3  23261  cxplim  23279  cxp2limlem  23283  cxploglim2  23286  jensenlem2  23295  jensen  23296  amgmlem  23297  emcllem2  23304  emcllem4  23306  emcllem7  23309  ftalem5  23328  basellem4  23335  basellem6  23337  basellem8  23339  basellem9  23340  chtwordi  23408  chpwordi  23409  ppiwordi  23414  ppiub  23457  vmalelog  23458  chtlepsi  23459  chtleppi  23463  chtublem  23464  chtub  23465  chpub  23473  logfaclbnd  23475  logfacrlim  23477  dchrptlem3  23519  bcmono  23530  bclbnd  23533  bposlem1  23537  bposlem6  23542  bposlem9  23545  lgsqrlem4  23597  chebbnd1lem1  23632  chebbnd1lem3  23634  chebbnd1  23635  chtppilimlem1  23636  vmadivsum  23645  rplogsumlem2  23648  dchrisumlema  23651  dchrisumlem3  23654  dchrmusum2  23657  dchrvmasumlem3  23662  dchrvmasumiflem1  23664  dchrisum0flblem1  23671  dchrisum0re  23676  dchrisum0lem2a  23680  mulogsumlem  23694  mulog2sumlem1  23697  mulog2sumlem2  23698  2vmadivsumlem  23703  selberg2lem  23713  selberg3lem1  23720  selberg4lem1  23723  pntrlog2bndlem3  23742  pntrlog2bndlem5  23744  pntrlog2bndlem6  23746  pntpbnd1  23749  pntlemc  23758  pntlemr  23765  pntlemk  23769  pntlemo  23770  abvcxp  23778  ostth2lem1  23781  padicabv  23793  ostth2lem2  23797  ostth2lem3  23798  ostth2lem4  23799  ostth2  23800  legso  23963  nvmtri  25552  imsmetlem  25574  vacn  25582  nmcvcn  25583  smcnlem  25585  blometi  25696  ipblnfi  25749  minvecolem2  25769  hhssnv  26158  nmcoplbi  26925  nmopcoi  26992  nmopcoadji  26998  idleop  27028  cdj1i  27330  isoun  27498  xlt2addrd  27556  omndmul  27682  ogrpsub  27685  archirngz  27711  gsumle  27748  ofldchr  27782  pstmxmet  27854  nexple  27983  esumpmono  28063  esumcvg  28070  meascnbl  28168  omsmon  28245  dstfrvinc  28393  zetacvg  28535  lgamgulmlem2  28550  lgamgulmlem5  28553  lgamcvg2  28575  derangenlem  28593  subfaclefac  28598  subfaclim  28610  erdszelem10  28622  sinccvglem  29016  iprodefisum  29100  itg2gt0cn  30046  ibladdnclem  30047  iblabsnc  30055  iblmulc2nc  30056  itgabsnc  30060  bddiblnc  30061  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  mettrifi  30226  equivbnd2  30264  heiborlem6  30288  bfplem1  30294  bfp  30296  rrnmet  30301  rrndstprj1  30302  rrndstprj2  30303  irrapxlem5  30738  pell1qrge1  30782  pell1qrgaplem  30785  pell14qrgapw  30788  pellqrex  30791  pellfund14  30810  expmordi  30859  jm2.17a  30874  jm2.17c  30876  acongeq  30897  jm2.19  30911  jm2.27a  30923  jm2.27c  30925  jm3.1lem2  30936  areaquad  31160  hashnzfzclim  31203  ltmod  31598  dvbdfbdioolem2  31680  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  stoweidlem3  31739  stoweidlem26  31762  wallispilem1  31801  wallispilem5  31805  stirlinglem1  31810  stirlinglem5  31814  stirlinglem8  31817  stirlinglem10  31819  stirlinglem12  31821  fourierdlem6  31849  fourierdlem7  31850  fourierdlem14  31857  fourierdlem19  31862  fourierdlem35  31878  fourierdlem39  31882  fourierdlem42  31885  fourierdlem50  31893  fourierdlem73  31916  fourierdlem76  31919  fourierdlem77  31920  fourierdlem81  31924  fourierdlem90  31933  fourierdlem92  31935  fourierdlem93  31936  fourierdlem111  31954  fouriersw  31968  rnghmsubcsetc  32660  rhmsubcsetc  32703  rhmsubcrngc  32709  rhmsubc  32766  rhmsubcOLD  32785  dalawlem3  35472  dalawlem4  35473  dalawlem6  35475  dalawlem9  35478  dalawlem11  35480  dalawlem12  35481  dalawlem15  35484  cdleme3c  35830  cdleme7e  35847  cdleme26e  35960  cdleme26eALTN  35962  cdleme27a  35968  cdleme32c  36044  cdleme32e  36046  cdleme32le  36048  cdlemg9b  36234  cdlemg12b  36245  cdlemg12d  36247  trlcolem  36327  trlcone  36329  cdlemk7  36449  cdlemk7u  36471  cdlemk39  36517  cdlemk11ta  36530  cdlemk11tc  36546  mapdcnvatN  37268  rp-isfinite6  37582
  Copyright terms: Public domain W3C validator