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

Theorem 3brtr4d 4234
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 4217 . 2  |-  ( ph  ->  ( C R D  <-> 
A R B ) )
51, 4mpbird 224 1  |-  ( ph  ->  C R D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   class class class wbr 4204
This theorem is referenced by:  f1oiso2  6064  sucdom2  7295  ordtypelem6  7484  cdaen  8045  cdacomen  8053  cdadom1  8058  fin23lem26  8197  distrnq  8830  lediv12a  9895  recp1lt1  9900  ifle  10775  xleadd1a  10824  xlemul1a  10859  quoremz  11228  quoremnn0ALT  11230  intfracq  11232  modmulnn  11257  fzennn  11299  monoord2  11346  expgt1  11410  leexp2r  11429  leexp1a  11430  bernneq  11497  expmulnbnd  11503  digit1  11505  faclbnd  11573  faclbnd4lem3  11578  faclbnd4lem4  11579  faclbnd6  11582  facubnd  11583  hashdomi  11646  fzsdom2  11685  absrele  12105  absimle  12106  abstri  12126  abs2difabs  12130  limsupval2  12266  rlimrege0  12365  rlimrecl  12366  climsqz  12426  climsqz2  12427  rlimdiv  12431  rlimsqz  12435  rlimsqz2  12436  isercolllem1  12450  isercoll2  12454  fsumcvg2  12513  fsumrlim  12582  o1fsum  12584  cvgcmpce  12589  isumle  12616  climcndslem1  12621  climcndslem2  12622  harmonic  12630  expcnv  12635  explecnv  12636  geomulcvg  12645  efcllem  12672  ege2le3  12684  eflegeo  12714  rpnnen2lem4  12809  ruclem2  12823  ruclem8  12828  fsumdvds  12885  phibnd  13152  iserodd  13201  pcdvdstr  13241  pcprmpw2  13247  pockthg  13266  prmreclem4  13279  2expltfac  13418  mod2ile  14527  odsubdvds  15197  pgpfi  15231  fislw  15251  efgredlemd  15368  efgredlem  15371  frgpcpbl  15383  abvres  15919  abvtrivd  15920  znrrg  16838  cstucnd  18306  psmetge0  18335  psmetres2  18337  xmetge0  18366  xmetres2  18383  imasf1oxmet  18397  comet  18535  stdbdxmet  18537  dscmet  18612  nrmmetd  18614  nmrtri  18662  tngngp  18687  nmolb2d  18744  nmoleub  18757  nmoco  18763  nmotri  18765  nmoid  18768  nmods  18770  cnmet  18798  xrsxmet  18832  metdstri  18873  metnrmlem3  18883  lebnumlem3  18980  ipcau2  19183  tchcphlem1  19184  tchcph  19186  minveclem2  19319  ovolunlem1a  19384  ovolscalem1  19401  voliunlem1  19436  volcn  19490  itg1climres  19598  mbfi1fseqlem5  19603  mbfi1fseqlem6  19604  itg2const2  19625  itg2seq  19626  itg2mulc  19631  itg2splitlem  19632  itg2monolem1  19634  itg2i1fseqle  19638  itg2i1fseq  19639  itg2i1fseq2  19640  itg2addlem  19642  itg2cnlem1  19645  itg2cnlem2  19646  iblss  19688  itgle  19693  ibladdlem  19703  iblabs  19712  iblabsr  19713  iblmulc2  19714  itgabs  19718  bddmulibl  19722  dvfsumabs  19899  dvfsumlem2  19903  dvfsum2  19910  deg1suble  20022  deg1mul3le  20031  plyeq0lem  20121  dgrcolem2  20184  geolim3  20248  aaliou3lem2  20252  aaliou3lem8  20254  ulmdvlem1  20308  radcnvlem1  20321  radcnvlem2  20322  dvradcnv  20329  pserulm  20330  pserdvlem2  20336  abelthlem2  20340  abelthlem5  20343  abelthlem7  20346  abelth2  20350  tangtx  20405  tanabsge  20406  tanord1  20431  argregt0  20497  argrege0  20498  argimgt0  20499  abslogle  20505  logcnlem4  20528  logtayllem  20542  abscxpbnd  20629  ang180lem2  20644  atanlogsublem  20747  atans2  20763  leibpi  20774  birthdaylem3  20784  cxplim  20802  cxp2limlem  20806  cxploglim2  20809  jensenlem2  20818  jensen  20819  amgmlem  20820  emcllem2  20827  emcllem4  20829  emcllem7  20832  ftalem5  20851  basellem4  20858  basellem6  20860  basellem8  20862  basellem9  20863  chtwordi  20931  chpwordi  20932  ppiwordi  20937  ppiub  20980  vmalelog  20981  chtlepsi  20982  chtleppi  20986  chtublem  20987  chtub  20988  chpub  20996  logfaclbnd  20998  logfacrlim  21000  bcmono  21053  bclbnd  21056  bposlem1  21060  bposlem6  21065  bposlem9  21068  lgsqrlem4  21120  chebbnd1lem1  21155  chebbnd1lem3  21157  chebbnd1  21158  chtppilimlem1  21159  vmadivsum  21168  rplogsumlem2  21171  dchrisumlema  21174  dchrisumlem3  21177  dchrmusum2  21180  dchrvmasumlem3  21185  dchrvmasumiflem1  21187  dchrisum0flblem1  21194  dchrisum0re  21199  dchrisum0lem2a  21203  mulogsumlem  21217  mulog2sumlem1  21220  mulog2sumlem2  21221  2vmadivsumlem  21226  selberg2lem  21236  selberg3lem1  21243  selberg4lem1  21246  pntrlog2bndlem3  21265  pntrlog2bndlem5  21267  pntrlog2bndlem6  21269  pntpbnd1  21272  pntlemc  21281  pntlemr  21288  pntlemk  21292  pntlemo  21293  abvcxp  21301  padicabv  21316  ostth2lem2  21320  ostth2lem3  21321  ostth2lem4  21322  ostth2  21323  nvmtri  22152  imsmetlem  22174  vacn  22182  nmcvcn  22183  smcnlem  22185  blometi  22296  ipblnfi  22349  minvecolem2  22369  hhssnv  22756  nmcoplbi  23523  nmopcoi  23590  nmopcoadji  23596  idleop  23626  cdj1i  23928  isoun  24081  xlt2addrd  24116  ofldchr  24236  esumpmono  24461  esumcvg  24468  meascnbl  24565  volss  24575  dstfrvinc  24726  zetacvg  24791  lgamgulmlem2  24806  lgamgulmlem5  24809  lgamcvg2  24831  derangenlem  24849  subfaclefac  24854  subfaclim  24866  erdszelem10  24878  sinccvglem  25101  iprodefisum  25310  itg2gt0cn  26250  ibladdnclem  26251  iblabsnc  26259  iblmulc2nc  26260  itgabsnc  26264  bddiblnc  26265  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  trirn  26448  mettrifi  26454  equivbnd2  26492  heiborlem6  26516  bfplem1  26522  bfp  26524  rrnmet  26529  rrndstprj1  26530  rrndstprj2  26531  irrapxlem5  26880  pell1qrge1  26924  pell1qrgaplem  26927  pell14qrgapw  26930  pellqrex  26933  pellfund14  26952  expmordi  27001  jm2.17a  27016  jm2.17c  27018  acongeq  27039  jm2.19  27055  jm2.27a  27067  jm2.27c  27069  jm3.1lem2  27080  stoweidlem3  27719  stoweidlem26  27742  wallispilem1  27781  wallispilem5  27785  stirlinglem1  27790  stirlinglem5  27794  stirlinglem8  27797  stirlinglem10  27799  stirlinglem12  27801  dalawlem3  30607  dalawlem4  30608  dalawlem6  30610  dalawlem9  30613  dalawlem11  30615  dalawlem12  30616  dalawlem15  30619  cdleme3c  30964  cdleme7e  30981  cdleme26e  31093  cdleme26eALTN  31095  cdleme27a  31101  cdleme32c  31177  cdleme32e  31179  cdleme32le  31181  cdlemg9b  31367  cdlemg12b  31378  cdlemg12d  31380  trlcolem  31460  trlcone  31462  cdlemk7  31582  cdlemk7u  31604  cdlemk39  31650  cdlemk11ta  31663  cdlemk11tc  31679  mapdcnvatN  32401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205
  Copyright terms: Public domain W3C validator