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

Theorem 3brtr4d 4397
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 4380 . 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 1399   class class class wbr 4367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368
This theorem is referenced by:  f1oiso2  6149  sucdom2  7632  ordtypelem6  7863  cdaen  8466  cdacomen  8474  cdadom1  8479  fin23lem26  8618  distrnq  9250  lediv12a  10354  recp1lt1  10359  ifle  11317  xleadd1a  11366  xlemul1a  11401  quoremz  11882  quoremnn0ALT  11884  intfracq  11886  modmulnn  11914  fzennn  11981  monoord2  12041  expgt1  12107  leexp2r  12126  leexp1a  12127  bernneq  12194  expmulnbnd  12200  digit1  12202  faclbnd  12270  faclbnd4lem3  12275  faclbnd4lem4  12276  faclbnd6  12279  facubnd  12280  hashdomi  12351  fzsdom2  12390  absrele  13143  absimle  13144  abstri  13165  abs2difabs  13169  limsupval2  13305  rlimrege0  13404  rlimrecl  13405  climsqz  13465  climsqz2  13466  rlimdiv  13470  rlimsqz  13474  rlimsqz2  13475  isercolllem1  13489  isercoll2  13493  fsumcvg2  13551  fsumrlim  13627  o1fsum  13629  cvgcmpce  13634  isumle  13658  climcndslem1  13663  climcndslem2  13664  harmonic  13672  expcnv  13677  explecnv  13678  geomulcvg  13687  efcllem  13815  ege2le3  13827  eflegeo  13858  rpnnen2lem4  13953  ruclem2  13967  ruclem8  13972  fsumdvds  14031  phibnd  14303  iserodd  14361  pcdvdstr  14401  pcprmpw2  14407  pockthg  14426  prmreclem4  14439  2expltfac  14579  mod2ile  15853  odsubdvds  16708  pgpfi  16742  fislw  16762  efgredlemd  16879  efgredlem  16882  frgpcpbl  16894  abvres  17601  abvtrivd  17602  znrrg  18695  cstucnd  20872  psmetge0  20901  psmetres2  20903  xmetge0  20932  xmetres2  20949  imasf1oxmet  20963  comet  21101  stdbdxmet  21103  dscmet  21178  nrmmetd  21180  nmrtri  21228  tngngp  21253  nmolb2d  21310  nmoleub  21323  nmoco  21329  nmotri  21331  nmoid  21334  nmods  21336  cnmet  21364  xrsxmet  21399  metdstri  21440  metnrmlem3  21450  lebnumlem3  21548  ipcau2  21762  tchcphlem1  21763  tchcph  21765  trirn  21912  rrxmet  21920  rrxdstprj1  21921  minveclem2  21926  ovolunlem1a  21992  ovolscalem1  22009  volss  22029  voliunlem1  22045  volcn  22100  itg1climres  22206  mbfi1fseqlem5  22211  mbfi1fseqlem6  22212  itg2const2  22233  itg2seq  22234  itg2mulc  22239  itg2splitlem  22240  itg2monolem1  22242  itg2i1fseqle  22246  itg2i1fseq  22247  itg2i1fseq2  22248  itg2addlem  22250  itg2cnlem1  22253  itg2cnlem2  22254  iblss  22296  itgle  22301  ibladdlem  22311  iblabs  22320  iblabsr  22321  iblmulc2  22322  itgabs  22326  bddmulibl  22330  dvfsumabs  22509  dvfsumlem2  22513  dvfsum2  22520  deg1suble  22593  deg1mul3le  22602  plyeq0lem  22692  dgrcolem2  22756  geolim3  22820  aaliou3lem2  22824  aaliou3lem8  22826  ulmdvlem1  22880  radcnvlem1  22893  radcnvlem2  22894  dvradcnv  22901  pserulm  22902  pserdvlem2  22908  abelthlem2  22912  abelthlem5  22915  abelthlem7  22918  abelth2  22922  tangtx  22983  tanabsge  22984  tanord1  23009  argregt0  23082  argrege0  23083  argimgt0  23084  abslogle  23090  logcnlem4  23113  logtayllem  23127  abscxpbnd  23214  ang180lem2  23260  atanlogsublem  23362  atans2  23378  leibpi  23389  birthdaylem3  23400  cxplim  23418  cxp2limlem  23422  cxploglim2  23425  jensenlem2  23434  jensen  23435  amgmlem  23436  emcllem2  23443  emcllem4  23445  emcllem7  23448  ftalem5  23467  basellem4  23474  basellem6  23476  basellem8  23478  basellem9  23479  chtwordi  23547  chpwordi  23548  ppiwordi  23553  ppiub  23596  vmalelog  23597  chtlepsi  23598  chtleppi  23602  chtublem  23603  chtub  23604  chpub  23612  logfaclbnd  23614  logfacrlim  23616  dchrptlem3  23658  bcmono  23669  bclbnd  23672  bposlem1  23676  bposlem6  23681  bposlem9  23684  lgsqrlem4  23736  chebbnd1lem1  23771  chebbnd1lem3  23773  chebbnd1  23774  chtppilimlem1  23775  vmadivsum  23784  rplogsumlem2  23787  dchrisumlema  23790  dchrisumlem3  23793  dchrmusum2  23796  dchrvmasumlem3  23801  dchrvmasumiflem1  23803  dchrisum0flblem1  23810  dchrisum0re  23815  dchrisum0lem2a  23819  mulogsumlem  23833  mulog2sumlem1  23836  mulog2sumlem2  23837  2vmadivsumlem  23842  selberg2lem  23852  selberg3lem1  23859  selberg4lem1  23862  pntrlog2bndlem3  23881  pntrlog2bndlem5  23883  pntrlog2bndlem6  23885  pntpbnd1  23888  pntlemc  23897  pntlemr  23904  pntlemk  23908  pntlemo  23909  abvcxp  23917  ostth2lem1  23920  padicabv  23932  ostth2lem2  23936  ostth2lem3  23937  ostth2lem4  23938  ostth2  23939  legso  24105  nvmtri  25691  imsmetlem  25713  vacn  25721  nmcvcn  25722  smcnlem  25724  blometi  25835  ipblnfi  25888  minvecolem2  25908  hhssnv  26297  nmcoplbi  27063  nmopcoi  27130  nmopcoadji  27136  idleop  27166  cdj1i  27468  isoun  27667  xlt2addrd  27728  omndmul  27857  ogrpsub  27860  archirngz  27886  gsumle  27923  ofldchr  27958  pstmxmet  28030  nexple  28158  esumpmono  28227  esumcvg  28234  meascnbl  28346  omsmon  28425  omsmeas  28450  dstfrvinc  28598  zetacvg  28746  lgamgulmlem2  28761  lgamgulmlem5  28764  lgamcvg2  28786  derangenlem  28804  subfaclefac  28809  subfaclim  28821  erdszelem10  28833  sinccvglem  29227  iprodefisum  29290  itg2gt0cn  30236  ibladdnclem  30237  iblabsnc  30245  iblmulc2nc  30246  itgabsnc  30250  bddiblnc  30251  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264  mettrifi  30416  equivbnd2  30454  heiborlem6  30478  bfplem1  30484  bfp  30486  rrnmet  30491  rrndstprj1  30492  rrndstprj2  30493  irrapxlem5  30927  pell1qrge1  30971  pell1qrgaplem  30974  pell14qrgapw  30977  pellqrex  30980  pellfund14  30999  expmordi  31048  jm2.17a  31063  jm2.17c  31065  acongeq  31086  jm2.19  31101  jm2.27a  31113  jm2.27c  31115  jm3.1lem2  31126  areaquad  31352  hashnzfzclim  31395  binomcxplemnotnn0  31429  ltmod  31810  dvbdfbdioolem2  31892  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  stoweidlem3  31951  stoweidlem26  31974  wallispilem1  32013  wallispilem5  32017  stirlinglem1  32022  stirlinglem5  32026  stirlinglem8  32029  stirlinglem10  32031  stirlinglem12  32033  fourierdlem6  32061  fourierdlem7  32062  fourierdlem14  32069  fourierdlem19  32074  fourierdlem35  32090  fourierdlem39  32094  fourierdlem42  32097  fourierdlem50  32105  fourierdlem73  32128  fourierdlem76  32131  fourierdlem77  32132  fourierdlem81  32136  fourierdlem90  32145  fourierdlem92  32147  fourierdlem93  32148  fourierdlem111  32166  fouriersw  32180  etransclem38  32221  rnghmsubcsetc  32985  rhmsubcsetc  33031  rhmsubcrngc  33037  rhmsubc  33098  rhmsubcALTV  33117  logbpw2m1  33388  dignn0flhalflem1  33436  dignn0flhalflem2  33437  dalawlem3  36010  dalawlem4  36011  dalawlem6  36013  dalawlem9  36016  dalawlem11  36018  dalawlem12  36019  dalawlem15  36022  cdleme3c  36368  cdleme7e  36385  cdleme26e  36498  cdleme26eALTN  36500  cdleme27a  36506  cdleme32c  36582  cdleme32e  36584  cdleme32le  36586  cdlemg9b  36772  cdlemg12b  36783  cdlemg12d  36785  trlcolem  36865  trlcone  36867  cdlemk7  36987  cdlemk7u  37009  cdlemk39  37055  cdlemk11ta  37068  cdlemk11tc  37084  mapdcnvatN  37806  rp-isfinite6  38173
  Copyright terms: Public domain W3C validator