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

Theorem 3brtr4d 4456
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 4439 . 2  |-  ( ph  ->  ( C R D  <-> 
A R B ) )
51, 4mpbird 235 1  |-  ( ph  ->  C R D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   class class class wbr 4426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427
This theorem is referenced by:  f1oiso2  6258  sucdom2  7774  ordtypelem6  8038  cdaen  8601  cdacomen  8609  cdadom1  8614  fin23lem26  8753  distrnq  9385  lediv12a  10499  recp1lt1  10504  ifle  11490  xleadd1a  11539  xlemul1a  11574  quoremz  12079  quoremnn0ALT  12081  intfracq  12083  modmulnn  12111  fzennn  12178  monoord2  12241  expgt1  12307  leexp2r  12327  leexp1a  12328  bernneq  12395  expmulnbnd  12401  digit1  12403  faclbnd  12472  faclbnd4lem3  12477  faclbnd4lem4  12478  faclbnd6  12481  facubnd  12482  hashdomi  12556  fzsdom2  12595  absrele  13350  absimle  13351  abstri  13372  abs2difabs  13376  limsupval2  13518  limsupval2OLD  13519  rlimrege0  13621  rlimrecl  13622  climsqz  13682  climsqz2  13683  rlimdiv  13687  rlimsqz  13691  rlimsqz2  13692  isercolllem1  13706  isercoll2  13710  fsumcvg2  13771  fsumrlim  13849  o1fsum  13851  cvgcmpce  13856  isumle  13880  climcndslem1  13885  climcndslem2  13886  harmonic  13895  expcnv  13900  explecnv  13901  geomulcvg  13910  efcllem  14110  ege2le3  14122  eflegeo  14153  rpnnen2lem4  14248  ruclem2  14262  ruclem8  14267  fsumdvds  14326  phibnd  14679  iserodd  14739  pcdvdstr  14779  pcprmpw2  14785  pockthg  14804  prmreclem4  14817  prmolefac  14958  prmorlefacOLD  14972  prmordvdslcmsOLDOLD  14975  2expltfac  15017  mod2ile  16294  odsubdvds  17149  pgpfi  17183  fislw  17203  efgredlemd  17320  efgredlem  17323  frgpcpbl  17335  abvres  17993  abvtrivd  17994  znrrg  19058  cstucnd  21221  psmetge0  21250  psmetres2  21252  xmetge0  21281  xmetres2  21298  imasf1oxmet  21312  comet  21450  stdbdxmet  21452  dscmet  21509  nrmmetd  21511  nmrtri  21559  tngngp  21584  nmolb2d  21641  nmoleub  21654  nmoco  21660  nmotri  21662  nmoid  21665  nmods  21667  cnmet  21694  xrsxmet  21729  metdstri  21770  metnrmlem3  21780  lebnumlem3  21878  ipcau2  22092  tchcphlem1  22093  tchcph  22095  trirn  22238  rrxmet  22246  rrxdstprj1  22247  minveclem2  22252  ovolunlem1a  22318  ovolscalem1  22335  volss  22355  voliunlem1  22371  volcn  22432  itg1climres  22540  mbfi1fseqlem5  22545  mbfi1fseqlem6  22546  itg2const2  22567  itg2seq  22568  itg2mulc  22573  itg2splitlem  22574  itg2monolem1  22576  itg2i1fseqle  22580  itg2i1fseq  22581  itg2i1fseq2  22582  itg2addlem  22584  itg2cnlem1  22587  itg2cnlem2  22588  iblss  22630  itgle  22635  ibladdlem  22645  iblabs  22654  iblabsr  22655  iblmulc2  22656  itgabs  22660  bddmulibl  22664  dvfsumabs  22843  dvfsumlem2  22847  dvfsum2  22854  deg1suble  22924  deg1mul3le  22933  plyeq0lem  23023  dgrcolem2  23087  geolim3  23151  aaliou3lem2  23155  aaliou3lem8  23157  ulmdvlem1  23211  radcnvlem1  23224  radcnvlem2  23225  dvradcnv  23232  pserulm  23233  pserdvlem2  23239  abelthlem2  23243  abelthlem5  23246  abelthlem7  23249  abelth2  23253  tangtx  23316  tanabsge  23317  tanord1  23342  argregt0  23415  argrege0  23416  argimgt0  23417  abslogle  23423  logcnlem4  23446  logtayllem  23460  abscxpbnd  23549  ang180lem2  23595  atanlogsublem  23697  atans2  23713  leibpi  23724  birthdaylem3  23735  cxplim  23753  cxp2limlem  23757  cxploglim2  23760  jensenlem2  23769  jensen  23770  amgmlem  23771  emcllem2  23778  emcllem4  23780  emcllem7  23783  zetacvg  23796  lgamgulmlem2  23811  lgamgulmlem5  23814  lgamcvg2  23836  ftalem5  23857  basellem4  23864  basellem6  23866  basellem8  23868  basellem9  23869  chtwordi  23937  chpwordi  23938  ppiwordi  23943  ppiub  23986  vmalelog  23987  chtlepsi  23988  chtleppi  23992  chtublem  23993  chtub  23994  chpub  24002  logfaclbnd  24004  logfacrlim  24006  dchrptlem3  24048  bcmono  24059  bclbnd  24062  bposlem1  24066  bposlem6  24071  bposlem9  24074  lgsqrlem4  24126  chebbnd1lem1  24161  chebbnd1lem3  24163  chebbnd1  24164  chtppilimlem1  24165  vmadivsum  24174  rplogsumlem2  24177  dchrisumlema  24180  dchrisumlem3  24183  dchrmusum2  24186  dchrvmasumlem3  24191  dchrvmasumiflem1  24193  dchrisum0flblem1  24200  dchrisum0re  24205  dchrisum0lem2a  24209  mulogsumlem  24223  mulog2sumlem1  24226  mulog2sumlem2  24227  2vmadivsumlem  24232  selberg2lem  24242  selberg3lem1  24249  selberg4lem1  24252  pntrlog2bndlem3  24271  pntrlog2bndlem5  24273  pntrlog2bndlem6  24275  pntpbnd1  24278  pntlemc  24287  pntlemr  24294  pntlemk  24298  pntlemo  24299  abvcxp  24307  ostth2lem1  24310  padicabv  24322  ostth2lem2  24326  ostth2lem3  24327  ostth2lem4  24328  ostth2  24329  legso  24495  trgcopy  24693  nvmtri  26136  imsmetlem  26158  vacn  26166  nmcvcn  26167  smcnlem  26169  blometi  26280  ipblnfi  26333  minvecolem2  26353  hhssnv  26741  nmcoplbi  27507  nmopcoi  27574  nmopcoadji  27580  idleop  27610  cdj1i  27912  isoun  28113  xlt2addrd  28170  omndmul  28306  ogrpsub  28309  archirngz  28335  gsumle  28371  ofldchr  28407  pstmxmet  28530  nexple  28661  esumpmono  28730  esumcvg  28737  meascnbl  28871  omsmon  28950  omsmeas  28975  dstfrvinc  29126  derangenlem  29673  subfaclefac  29678  subfaclim  29690  erdszelem10  29702  sinccvglem  30095  iprodefisum  30155  itg2gt0cn  31691  ibladdnclem  31692  iblabsnc  31700  iblmulc2nc  31701  itgabsnc  31705  bddiblnc  31706  ftc1anclem7  31717  ftc1anclem8  31718  ftc1anc  31719  mettrifi  31780  equivbnd2  31818  heiborlem6  31842  bfplem1  31848  bfp  31850  rrnmet  31855  rrndstprj1  31856  rrndstprj2  31857  dalawlem3  33137  dalawlem4  33138  dalawlem6  33140  dalawlem9  33143  dalawlem11  33145  dalawlem12  33146  dalawlem15  33149  cdleme3c  33495  cdleme7e  33512  cdleme26e  33625  cdleme26eALTN  33627  cdleme27a  33633  cdleme32c  33709  cdleme32e  33711  cdleme32le  33713  cdlemg9b  33899  cdlemg12b  33910  cdlemg12d  33912  trlcolem  33992  trlcone  33994  cdlemk7  34114  cdlemk7u  34136  cdlemk39  34182  cdlemk11ta  34195  cdlemk11tc  34211  mapdcnvatN  34933  irrapxlem5  35370  pell1qrge1  35414  pell1qrgaplem  35417  pell14qrgapw  35420  pellqrex  35423  pellfund14  35442  expmordi  35491  jm2.17a  35506  jm2.17c  35508  acongeq  35529  jm2.19  35544  jm2.27a  35556  jm2.27c  35558  jm3.1lem2  35569  areaquad  35790  rp-isfinite6  35852  hashnzfzclim  36298  binomcxplemnotnn0  36332  ltmod  37280  dvbdfbdioolem2  37363  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  stoweidlem3  37422  stoweidlem26  37445  wallispilem1  37486  wallispilem5  37490  stirlinglem1  37495  stirlinglem5  37499  stirlinglem8  37502  stirlinglem10  37504  stirlinglem12  37506  fourierdlem6  37534  fourierdlem7  37535  fourierdlem14  37542  fourierdlem19  37547  fourierdlem35  37563  fourierdlem39  37567  fourierdlem42  37570  fourierdlem50  37578  fourierdlem73  37601  fourierdlem76  37604  fourierdlem77  37605  fourierdlem81  37609  fourierdlem90  37618  fourierdlem92  37620  fourierdlem93  37621  fourierdlem111  37639  fouriersw  37653  etransclem38  37694  sge0split  37775  rnghmsubcsetc  38727  rhmsubcsetc  38773  rhmsubcrngc  38779  rhmsubc  38840  rhmsubcALTV  38859  logbpw2m1  39129  dignn0flhalflem1  39177  dignn0flhalflem2  39178
  Copyright terms: Public domain W3C validator