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

Theorem 3brtr4d 4202
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 4185 . 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 1649   class class class wbr 4172
This theorem is referenced by:  f1oiso2  6031  sucdom2  7262  ordtypelem6  7448  cdaen  8009  cdacomen  8017  cdadom1  8022  fin23lem26  8161  distrnq  8794  lediv12a  9859  recp1lt1  9864  ifle  10739  xleadd1a  10788  xlemul1a  10823  quoremz  11191  quoremnn0ALT  11193  intfracq  11195  modmulnn  11220  fzennn  11262  monoord2  11309  expgt1  11373  leexp2r  11392  leexp1a  11393  bernneq  11460  expmulnbnd  11466  digit1  11468  faclbnd  11536  faclbnd4lem3  11541  faclbnd4lem4  11542  faclbnd6  11545  facubnd  11546  hashdomi  11609  fzsdom2  11648  absrele  12068  absimle  12069  abstri  12089  abs2difabs  12093  limsupval2  12229  rlimrege0  12328  rlimrecl  12329  climsqz  12389  climsqz2  12390  rlimdiv  12394  rlimsqz  12398  rlimsqz2  12399  isercolllem1  12413  isercoll2  12417  fsumcvg2  12476  fsumrlim  12545  o1fsum  12547  cvgcmpce  12552  isumle  12579  climcndslem1  12584  climcndslem2  12585  harmonic  12593  expcnv  12598  explecnv  12599  geomulcvg  12608  efcllem  12635  ege2le3  12647  eflegeo  12677  rpnnen2lem4  12772  ruclem2  12786  ruclem8  12791  fsumdvds  12848  phibnd  13115  iserodd  13164  pcdvdstr  13204  pcprmpw2  13210  pockthg  13229  prmreclem4  13242  2expltfac  13381  mod2ile  14490  odsubdvds  15160  pgpfi  15194  fislw  15214  efgredlemd  15331  efgredlem  15334  frgpcpbl  15346  abvres  15882  abvtrivd  15883  znrrg  16801  cstucnd  18267  psmetge0  18296  psmetres2  18298  xmetge0  18327  xmetres2  18344  imasf1oxmet  18358  comet  18496  stdbdxmet  18498  dscmet  18573  nrmmetd  18575  nmrtri  18623  tngngp  18648  nmolb2d  18705  nmoleub  18718  nmoco  18724  nmotri  18726  nmoid  18729  nmods  18731  cnmet  18759  xrsxmet  18793  metdstri  18834  metnrmlem3  18844  lebnumlem3  18941  ipcau2  19144  tchcphlem1  19145  tchcph  19147  minveclem2  19280  ovolunlem1a  19345  ovolscalem1  19362  voliunlem1  19397  volcn  19451  itg1climres  19559  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  itg2const2  19586  itg2seq  19587  itg2mulc  19592  itg2splitlem  19593  itg2monolem1  19595  itg2i1fseqle  19599  itg2i1fseq  19600  itg2i1fseq2  19601  itg2addlem  19603  itg2cnlem1  19606  itg2cnlem2  19607  iblss  19649  itgle  19654  ibladdlem  19664  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgabs  19679  bddmulibl  19683  dvfsumabs  19860  dvfsumlem2  19864  dvfsum2  19871  deg1suble  19983  deg1mul3le  19992  plyeq0lem  20082  dgrcolem2  20145  geolim3  20209  aaliou3lem2  20213  aaliou3lem8  20215  ulmdvlem1  20269  radcnvlem1  20282  radcnvlem2  20283  dvradcnv  20290  pserulm  20291  pserdvlem2  20297  abelthlem2  20301  abelthlem5  20304  abelthlem7  20307  abelth2  20311  tangtx  20366  tanabsge  20367  tanord1  20392  argregt0  20458  argrege0  20459  argimgt0  20460  abslogle  20466  logcnlem4  20489  logtayllem  20503  abscxpbnd  20590  ang180lem2  20605  atanlogsublem  20708  atans2  20724  leibpi  20735  birthdaylem3  20745  cxplim  20763  cxp2limlem  20767  cxploglim2  20770  jensenlem2  20779  jensen  20780  amgmlem  20781  emcllem2  20788  emcllem4  20790  emcllem7  20793  ftalem5  20812  basellem4  20819  basellem6  20821  basellem8  20823  basellem9  20824  chtwordi  20892  chpwordi  20893  ppiwordi  20898  ppiub  20941  vmalelog  20942  chtlepsi  20943  chtleppi  20947  chtublem  20948  chtub  20949  chpub  20957  logfaclbnd  20959  logfacrlim  20961  bcmono  21014  bclbnd  21017  bposlem1  21021  bposlem6  21026  bposlem9  21029  lgsqrlem4  21081  chebbnd1lem1  21116  chebbnd1lem3  21118  chebbnd1  21119  chtppilimlem1  21120  vmadivsum  21129  rplogsumlem2  21132  dchrisumlema  21135  dchrisumlem3  21138  dchrmusum2  21141  dchrvmasumlem3  21146  dchrvmasumiflem1  21148  dchrisum0flblem1  21155  dchrisum0re  21160  dchrisum0lem2a  21164  mulogsumlem  21178  mulog2sumlem1  21181  mulog2sumlem2  21182  2vmadivsumlem  21187  selberg2lem  21197  selberg3lem1  21204  selberg4lem1  21207  pntrlog2bndlem3  21226  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntpbnd1  21233  pntlemc  21242  pntlemr  21249  pntlemk  21253  pntlemo  21254  abvcxp  21262  padicabv  21277  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth2  21284  nvmtri  22113  imsmetlem  22135  vacn  22143  nmcvcn  22144  smcnlem  22146  blometi  22257  ipblnfi  22310  minvecolem2  22330  hhssnv  22717  nmcoplbi  23484  nmopcoi  23551  nmopcoadji  23557  idleop  23587  cdj1i  23889  isoun  24042  xlt2addrd  24077  ofldchr  24197  esumpmono  24422  esumcvg  24429  meascnbl  24526  volss  24536  dstfrvinc  24687  zetacvg  24752  lgamgulmlem2  24767  lgamgulmlem5  24770  lgamcvg2  24792  derangenlem  24810  subfaclefac  24815  subfaclim  24827  erdszelem10  24839  sinccvglem  25062  iprodefisum  25271  itg2gt0cn  26159  ibladdnclem  26160  iblabsnc  26168  iblmulc2nc  26169  itgabsnc  26173  bddiblnc  26174  trirn  26347  mettrifi  26353  equivbnd2  26391  heiborlem6  26415  bfplem1  26421  bfp  26423  rrnmet  26428  rrndstprj1  26429  rrndstprj2  26430  irrapxlem5  26779  pell1qrge1  26823  pell1qrgaplem  26826  pell14qrgapw  26829  pellqrex  26832  pellfund14  26851  expmordi  26900  jm2.17a  26915  jm2.17c  26917  acongeq  26938  jm2.19  26954  jm2.27a  26966  jm2.27c  26968  jm3.1lem2  26979  stoweidlem3  27619  stoweidlem26  27642  wallispilem1  27681  wallispilem5  27685  stirlinglem1  27690  stirlinglem5  27694  stirlinglem8  27697  stirlinglem10  27699  stirlinglem12  27701  swrdccat3b  28031  dalawlem3  30355  dalawlem4  30356  dalawlem6  30358  dalawlem9  30361  dalawlem11  30363  dalawlem12  30364  dalawlem15  30367  cdleme3c  30712  cdleme7e  30729  cdleme26e  30841  cdleme26eALTN  30843  cdleme27a  30849  cdleme32c  30925  cdleme32e  30927  cdleme32le  30929  cdlemg9b  31115  cdlemg12b  31126  cdlemg12d  31128  trlcolem  31208  trlcone  31210  cdlemk7  31330  cdlemk7u  31352  cdlemk39  31398  cdlemk11ta  31411  cdlemk11tc  31427  mapdcnvatN  32149
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173
  Copyright terms: Public domain W3C validator