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

Theorem 3brtr4d 4069
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 4052 . 2  |-  ( ph  ->  ( C R D  <-> 
A R B ) )
51, 4mpbird 223 1  |-  ( ph  ->  C R D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   class class class wbr 4039
This theorem is referenced by:  f1oiso2  5865  sucdom2  7073  ordtypelem6  7254  cdaen  7815  cdacomen  7823  cdadom1  7828  fin23lem26  7967  distrnq  8601  lediv12a  9665  recp1lt1  9670  ifle  10540  xleadd1a  10589  xlemul1a  10624  quoremz  10975  quoremnn0ALT  10977  intfracq  10979  modmulnn  11004  fzennn  11046  monoord2  11093  expgt1  11156  leexp2r  11175  leexp1a  11176  bernneq  11243  expmulnbnd  11249  digit1  11251  faclbnd  11319  faclbnd4lem3  11324  faclbnd4lem4  11325  faclbnd6  11328  facubnd  11329  hashdomi  11378  fzsdom2  11398  absrele  11809  absimle  11810  abstri  11830  abs2difabs  11834  limsupval2  11970  rlimrege0  12069  rlimrecl  12070  climsqz  12130  climsqz2  12131  rlimdiv  12135  rlimsqz  12139  rlimsqz2  12140  isercolllem1  12154  isercoll2  12158  fsumcvg2  12216  fsumrlim  12285  o1fsum  12287  cvgcmpce  12292  isumle  12319  climcndslem1  12324  climcndslem2  12325  harmonic  12333  expcnv  12338  explecnv  12339  geomulcvg  12348  efcllem  12375  ege2le3  12387  eflegeo  12417  rpnnen2lem4  12512  ruclem2  12526  ruclem8  12531  fsumdvds  12588  phibnd  12855  iserodd  12904  pcdvdstr  12944  pcprmpw2  12950  pockthg  12969  prmreclem4  12982  2expltfac  13121  mod2ile  14228  odsubdvds  14898  pgpfi  14932  fislw  14952  efgredlemd  15069  efgredlem  15072  frgpcpbl  15084  abvres  15620  abvtrivd  15621  znrrg  16535  xmetge0  17925  xmetres2  17941  imasf1oxmet  17955  comet  18075  stdbdxmet  18077  dscmet  18111  nrmmetd  18113  nmrtri  18161  tngngp  18186  nmolb2d  18243  nmoleub  18256  nmoco  18262  nmotri  18264  nmoid  18267  nmods  18269  cnmet  18297  xrsxmet  18331  metdstri  18371  metnrmlem3  18381  lebnumlem3  18477  ipcau2  18680  tchcphlem1  18681  tchcph  18683  minveclem2  18806  ovolunlem1a  18871  ovolscalem1  18888  voliunlem1  18923  volcn  18977  itg1climres  19085  mbfi1fseqlem5  19090  mbfi1fseqlem6  19091  itg2const2  19112  itg2seq  19113  itg2mulc  19118  itg2splitlem  19119  itg2monolem1  19121  itg2i1fseqle  19125  itg2i1fseq  19126  itg2i1fseq2  19127  itg2addlem  19129  itg2cnlem1  19132  itg2cnlem2  19133  iblss  19175  itgle  19180  ibladdlem  19190  iblabs  19199  iblabsr  19200  iblmulc2  19201  itgabs  19205  bddmulibl  19209  dvfsumabs  19386  dvfsumlem2  19390  dvfsum2  19397  deg1suble  19509  deg1mul3le  19518  plyeq0lem  19608  dgrcolem2  19671  geolim3  19735  aaliou3lem2  19739  aaliou3lem8  19741  ulmdvlem1  19793  radcnvlem1  19805  radcnvlem2  19806  dvradcnv  19813  pserulm  19814  pserdvlem2  19820  abelthlem2  19824  abelthlem5  19827  abelthlem7  19830  abelth2  19834  tangtx  19889  tanabsge  19890  tanord1  19915  argregt0  19980  argrege0  19981  argimgt0  19982  logcnlem4  20008  logtayllem  20022  abscxpbnd  20109  ang180lem2  20124  atanlogsublem  20227  atans2  20243  leibpi  20254  birthdaylem3  20264  cxplim  20282  cxp2limlem  20286  cxploglim2  20289  jensenlem2  20298  jensen  20299  amgmlem  20300  emcllem2  20306  emcllem4  20308  emcllem7  20311  ftalem5  20330  basellem4  20337  basellem6  20339  basellem8  20341  basellem9  20342  chtwordi  20410  chpwordi  20411  ppiwordi  20416  ppiub  20459  vmalelog  20460  chtlepsi  20461  chtleppi  20465  chtublem  20466  chtub  20467  chpub  20475  logfaclbnd  20477  logfacrlim  20479  bcmono  20532  bclbnd  20535  bposlem1  20539  bposlem6  20544  bposlem9  20547  lgsqrlem4  20599  chebbnd1lem1  20634  chebbnd1lem3  20636  chebbnd1  20637  chtppilimlem1  20638  vmadivsum  20647  rplogsumlem2  20650  dchrisumlema  20653  dchrisumlem3  20656  dchrmusum2  20659  dchrvmasumlem3  20664  dchrvmasumiflem1  20666  dchrisum0flblem1  20673  dchrisum0re  20678  dchrisum0lem2a  20682  mulogsumlem  20696  mulog2sumlem1  20699  mulog2sumlem2  20700  2vmadivsumlem  20705  selberg2lem  20715  selberg3lem1  20722  selberg4lem1  20725  pntrlog2bndlem3  20744  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntpbnd1  20751  pntlemc  20760  pntlemr  20767  pntlemk  20771  pntlemo  20772  abvcxp  20780  padicabv  20795  ostth2lem2  20799  ostth2lem3  20800  ostth2lem4  20801  ostth2  20802  nvmtri  21253  imsmetlem  21275  vacn  21283  nmcvcn  21284  smcnlem  21286  blometi  21397  ipblnfi  21450  minvecolem2  21470  hhssnv  21857  nmcoplbi  22624  nmopcoi  22691  nmopcoadji  22697  idleop  22727  cdj1i  23029  esumpmono  23462  esumcvg  23469  dstfrvinc  23692  zetacvg  23704  derangenlem  23717  subfaclefac  23722  subfaclim  23734  erdszelem10  23746  sinccvglem  24020  itg2gt0cn  25006  ibladdnclem  25007  iblabsnc  25015  iblmulc2nc  25016  itgabsnc  25020  bddiblnc  25021  cntrset  25705  mslb1  25710  trirn  26566  mettrifi  26576  equivbnd2  26619  heiborlem6  26643  bfplem1  26649  bfp  26651  rrnmet  26656  rrndstprj1  26657  rrndstprj2  26658  irrapxlem5  27014  pell1qrge1  27058  pell1qrgaplem  27061  pell14qrgapw  27064  pellqrex  27067  pellfund14  27086  expmordi  27135  jm2.17a  27150  jm2.17c  27152  acongeq  27173  jm2.19  27189  jm2.27a  27201  jm2.27c  27203  jm3.1lem2  27214  stoweidlem3  27855  wallispilem1  27917  wallispilem5  27921  stirlinglem1  27926  stirlinglem5  27930  stirlinglem8  27933  stirlinglem10  27935  stirlinglem11  27936  dalawlem3  30684  dalawlem4  30685  dalawlem6  30687  dalawlem9  30690  dalawlem11  30692  dalawlem12  30693  dalawlem15  30696  cdleme3c  31041  cdleme7e  31058  cdleme26e  31170  cdleme26eALTN  31172  cdleme27a  31178  cdleme32c  31254  cdleme32e  31256  cdleme32le  31258  cdlemg9b  31444  cdlemg12b  31455  cdlemg12d  31457  trlcolem  31537  trlcone  31539  cdlemk7  31659  cdlemk7u  31681  cdlemk39  31727  cdlemk11ta  31740  cdlemk11tc  31756  mapdcnvatN  32478
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator