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

Theorem 3brtr4d 4472
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 4455 . 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 1374   class class class wbr 4442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-br 4443
This theorem is referenced by:  f1oiso2  6229  sucdom2  7706  ordtypelem6  7939  cdaen  8544  cdacomen  8552  cdadom1  8557  fin23lem26  8696  distrnq  9330  lediv12a  10429  recp1lt1  10434  ifle  11387  xleadd1a  11436  xlemul1a  11471  quoremz  11940  quoremnn0ALT  11942  intfracq  11944  modmulnn  11971  fzennn  12036  monoord2  12096  expgt1  12161  leexp2r  12180  leexp1a  12181  bernneq  12249  expmulnbnd  12255  digit1  12257  faclbnd  12325  faclbnd4lem3  12330  faclbnd4lem4  12331  faclbnd6  12334  facubnd  12335  hashdomi  12405  fzsdom2  12440  absrele  13093  absimle  13094  abstri  13114  abs2difabs  13118  limsupval2  13254  rlimrege0  13353  rlimrecl  13354  climsqz  13414  climsqz2  13415  rlimdiv  13419  rlimsqz  13423  rlimsqz2  13424  isercolllem1  13438  isercoll2  13442  fsumcvg2  13500  fsumrlim  13576  o1fsum  13578  cvgcmpce  13583  isumle  13610  climcndslem1  13615  climcndslem2  13616  harmonic  13624  expcnv  13629  explecnv  13630  geomulcvg  13639  efcllem  13666  ege2le3  13678  eflegeo  13708  rpnnen2lem4  13803  ruclem2  13817  ruclem8  13822  fsumdvds  13879  phibnd  14151  iserodd  14209  pcdvdstr  14249  pcprmpw2  14255  pockthg  14274  prmreclem4  14287  2expltfac  14426  mod2ile  15584  odsubdvds  16382  pgpfi  16416  fislw  16436  efgredlemd  16553  efgredlem  16556  frgpcpbl  16568  abvres  17266  abvtrivd  17267  znrrg  18366  cstucnd  20517  psmetge0  20546  psmetres2  20548  xmetge0  20577  xmetres2  20594  imasf1oxmet  20608  comet  20746  stdbdxmet  20748  dscmet  20823  nrmmetd  20825  nmrtri  20873  tngngp  20898  nmolb2d  20955  nmoleub  20968  nmoco  20974  nmotri  20976  nmoid  20979  nmods  20981  cnmet  21009  xrsxmet  21044  metdstri  21085  metnrmlem3  21095  lebnumlem3  21193  ipcau2  21407  tchcphlem1  21408  tchcph  21410  trirn  21557  rrxmet  21565  rrxdstprj1  21566  minveclem2  21571  ovolunlem1a  21637  ovolscalem1  21654  volss  21674  voliunlem1  21690  volcn  21745  itg1climres  21851  mbfi1fseqlem5  21856  mbfi1fseqlem6  21857  itg2const2  21878  itg2seq  21879  itg2mulc  21884  itg2splitlem  21885  itg2monolem1  21887  itg2i1fseqle  21891  itg2i1fseq  21892  itg2i1fseq2  21893  itg2addlem  21895  itg2cnlem1  21898  itg2cnlem2  21899  iblss  21941  itgle  21946  ibladdlem  21956  iblabs  21965  iblabsr  21966  iblmulc2  21967  itgabs  21971  bddmulibl  21975  dvfsumabs  22154  dvfsumlem2  22158  dvfsum2  22165  deg1suble  22238  deg1mul3le  22247  plyeq0lem  22337  dgrcolem2  22400  geolim3  22464  aaliou3lem2  22468  aaliou3lem8  22470  ulmdvlem1  22524  radcnvlem1  22537  radcnvlem2  22538  dvradcnv  22545  pserulm  22546  pserdvlem2  22552  abelthlem2  22556  abelthlem5  22559  abelthlem7  22562  abelth2  22566  tangtx  22626  tanabsge  22627  tanord1  22652  argregt0  22718  argrege0  22719  argimgt0  22720  abslogle  22726  logcnlem4  22749  logtayllem  22763  abscxpbnd  22850  ang180lem2  22865  atanlogsublem  22969  atans2  22985  leibpi  22996  birthdaylem3  23006  cxplim  23024  cxp2limlem  23028  cxploglim2  23031  jensenlem2  23040  jensen  23041  amgmlem  23042  emcllem2  23049  emcllem4  23051  emcllem7  23054  ftalem5  23073  basellem4  23080  basellem6  23082  basellem8  23084  basellem9  23085  chtwordi  23153  chpwordi  23154  ppiwordi  23159  ppiub  23202  vmalelog  23203  chtlepsi  23204  chtleppi  23208  chtublem  23209  chtub  23210  chpub  23218  logfaclbnd  23220  logfacrlim  23222  dchrptlem3  23264  bcmono  23275  bclbnd  23278  bposlem1  23282  bposlem6  23287  bposlem9  23290  lgsqrlem4  23342  chebbnd1lem1  23377  chebbnd1lem3  23379  chebbnd1  23380  chtppilimlem1  23381  vmadivsum  23390  rplogsumlem2  23393  dchrisumlema  23396  dchrisumlem3  23399  dchrmusum2  23402  dchrvmasumlem3  23407  dchrvmasumiflem1  23409  dchrisum0flblem1  23416  dchrisum0re  23421  dchrisum0lem2a  23425  mulogsumlem  23439  mulog2sumlem1  23442  mulog2sumlem2  23443  2vmadivsumlem  23448  selberg2lem  23458  selberg3lem1  23465  selberg4lem1  23468  pntrlog2bndlem3  23487  pntrlog2bndlem5  23489  pntrlog2bndlem6  23491  pntpbnd1  23494  pntlemc  23503  pntlemr  23510  pntlemk  23514  pntlemo  23515  abvcxp  23523  padicabv  23538  ostth2lem2  23542  ostth2lem3  23543  ostth2lem4  23544  ostth2  23545  legso  23707  nvmtri  25238  imsmetlem  25260  vacn  25268  nmcvcn  25269  smcnlem  25271  blometi  25382  ipblnfi  25435  minvecolem2  25455  hhssnv  25844  nmcoplbi  26611  nmopcoi  26678  nmopcoadji  26684  idleop  26714  cdj1i  27016  isoun  27180  xlt2addrd  27234  omndmul  27354  ogrpsub  27357  archirngz  27383  gsumle  27421  ofldchr  27455  nexple  27633  esumpmono  27713  esumcvg  27720  meascnbl  27818  omsmon  27895  dstfrvinc  28043  zetacvg  28185  lgamgulmlem2  28200  lgamgulmlem5  28203  lgamcvg2  28225  derangenlem  28243  subfaclefac  28248  subfaclim  28260  erdszelem10  28272  sinccvglem  28501  iprodefisum  28689  itg2gt0cn  29636  ibladdnclem  29637  iblabsnc  29645  iblmulc2nc  29646  itgabsnc  29650  bddiblnc  29651  ftc1anclem7  29662  ftc1anclem8  29663  ftc1anc  29664  mettrifi  29842  equivbnd2  29880  heiborlem6  29904  bfplem1  29910  bfp  29912  rrnmet  29917  rrndstprj1  29918  rrndstprj2  29919  irrapxlem5  30355  pell1qrge1  30399  pell1qrgaplem  30402  pell14qrgapw  30405  pellqrex  30408  pellfund14  30427  expmordi  30476  jm2.17a  30491  jm2.17c  30493  acongeq  30514  jm2.19  30530  jm2.27a  30542  jm2.27c  30544  jm3.1lem2  30555  areaquad  30780  stoweidlem3  31260  stoweidlem26  31283  wallispilem1  31322  wallispilem5  31326  stirlinglem1  31331  stirlinglem5  31335  stirlinglem8  31338  stirlinglem10  31340  stirlinglem12  31342  fourierdlem93  31457  dalawlem3  34546  dalawlem4  34547  dalawlem6  34549  dalawlem9  34552  dalawlem11  34554  dalawlem12  34555  dalawlem15  34558  cdleme3c  34903  cdleme7e  34920  cdleme26e  35032  cdleme26eALTN  35034  cdleme27a  35040  cdleme32c  35116  cdleme32e  35118  cdleme32le  35120  cdlemg9b  35306  cdlemg12b  35317  cdlemg12d  35319  trlcolem  35399  trlcone  35401  cdlemk7  35521  cdlemk7u  35543  cdlemk39  35589  cdlemk11ta  35602  cdlemk11tc  35618  mapdcnvatN  36340
  Copyright terms: Public domain W3C validator