Theorem 3brtr4d 4685

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

Step	Hyp	Ref	Expression
1		3brtr4d.1	. 2 |- ( ph -> A R B )
2		3brtr4d.2	. . 3 |- ( ph -> C = A )
3		3brtr4d.3	. . 3 |- ( ph -> D = B )
4	2, 3	breq12d 4666	. 2 |- ( ph -> ( C R D <-> A R B ) )
5	1, 4	mpbird 247	1 |- ( ph -> C R D )

Syntax hints:   -> wi 4   = wceq 1483   class class class wbr 4653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654

This theorem is referenced by:  f1oiso2  6602  sucdom2  8156  ordtypelem6  8428  cdaen  8995  cdacomen  9003  cdadom1  9008  fin23lem26  9147  distrnq  9783  lediv12a  10916  recp1lt1  10921  ifle  12028  xleadd1a  12083  xlemul1a  12118  fldiv4p1lem1div2  12636  fldiv4lem1div2  12638  quoremz  12654  quoremnn0ALT  12656  intfracq  12658  modmulnn  12688  fzennn  12767  monoord2  12832  expgt1  12898  leexp2r  12918  leexp1a  12919  bernneq  12990  expmulnbnd  12996  digit1  12998  faclbnd  13077  faclbnd4lem3  13082  faclbnd4lem4  13083  faclbnd6  13086  facubnd  13087  hashdomi  13169  fzsdom2  13215  absrele  14048  absimle  14049  abstri  14070  abs2difabs  14074  limsupval2  14211  rlimrege0  14310  rlimrecl  14311  climsqz  14371  climsqz2  14372  rlimdiv  14376  rlimsqz  14380  rlimsqz2  14381  isercolllem1  14395  isercoll2  14399  fsumcvg2  14458  fsumrlim  14543  o1fsum  14545  cvgcmpce  14550  isumle  14576  climcndslem1  14581  climcndslem2  14582  harmonic  14591  expcnv  14596  explecnv  14597  geomulcvg  14607  efcllem  14808  ege2le3  14820  eflegeo  14851  rpnnen2lem4  14946  ruclem2  14961  ruclem8  14966  fsumdvds  15030  phibnd  15476  iserodd  15540  pcdvdstr  15580  pcprmpw2  15586  pockthg  15610  prmreclem4  15623  prmolefac  15750  2expltfac  15799  mod2ile  17106  odsubdvds  17986  pgpfi  18020  fislw  18040  efgredlemd  18157  efgredlem  18160  frgpcpbl  18172  abvres  18839  abvtrivd  18840  znrrg  19914  cstucnd  22088  psmetge0  22117  psmetres2  22119  xmetge0  22149  xmetres2  22166  imasf1oxmet  22180  comet  22318  stdbdxmet  22320  dscmet  22377  nrmmetd  22379  nmrtri  22428  tngngp  22458  nmolb2d  22522  nmoleub  22535  nmoco  22541  nmotri  22543  nmoid  22546  nmods  22548  cnmet  22575  xrsxmet  22612  metdstri  22654  metnrmlem3  22664  lebnumlem3  22762  ipcau2  23033  tchcphlem1  23034  tchcph  23036  trirn  23183  rrxmet  23191  rrxdstprj1  23192  minveclem2  23197  ovolunlem1a  23264  ovolscalem1  23281  volss  23301  voliunlem1  23318  volcn  23374  itg1climres  23481  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  itg2const2  23508  itg2seq  23509  itg2mulc  23514  itg2splitlem  23515  itg2monolem1  23517  itg2i1fseqle  23521  itg2i1fseq  23522  itg2i1fseq2  23523  itg2addlem  23525  itg2cnlem1  23528  itg2cnlem2  23529  iblss  23571  itgle  23576  ibladdlem  23586  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgabs  23601  bddmulibl  23605  dvfsumabs  23786  dvfsumlem2  23790  dvfsum2  23797  deg1suble  23867  deg1mul3le  23876  plyeq0lem  23966  dgrcolem2  24030  geolim3  24094  aaliou3lem2  24098  aaliou3lem8  24100  ulmdvlem1  24154  radcnvlem1  24167  radcnvlem2  24168  dvradcnv  24175  pserulm  24176  pserdvlem2  24182  abelthlem2  24186  abelthlem5  24189  abelthlem7  24192  abelth2  24196  tangtx  24257  tanabsge  24258  tanord1  24283  argregt0  24356  argrege0  24357  argimgt0  24358  abslogle  24364  logcnlem4  24391  logtayllem  24405  abscxpbnd  24494  ang180lem2  24540  atanlogsublem  24642  atans2  24658  leibpi  24669  birthdaylem3  24680  cxplim  24698  cxp2limlem  24702  cxploglim2  24705  jensenlem2  24714  jensen  24715  amgmlem  24716  emcllem2  24723  emcllem4  24725  emcllem7  24728  zetacvg  24741  lgamgulmlem2  24756  lgamgulmlem5  24759  lgamcvg2  24781  ftalem5  24803  basellem4  24810  basellem6  24812  basellem8  24814  basellem9  24815  chtwordi  24882  chpwordi  24883  ppiwordi  24888  ppiub  24929  vmalelog  24930  chtlepsi  24931  chtleppi  24935  chtublem  24936  chtub  24937  chpub  24945  logfaclbnd  24947  logfacrlim  24949  dchrptlem3  24991  bcmono  25002  bclbnd  25005  bposlem1  25009  bposlem6  25014  bposlem9  25017  lgsqrlem4  25074  2lgslem1c  25118  chebbnd1lem1  25158  chebbnd1lem3  25160  chebbnd1  25161  chtppilimlem1  25162  vmadivsum  25171  rplogsumlem2  25174  dchrisumlema  25177  dchrisumlem3  25180  dchrmusum2  25183  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  dchrisum0re  25202  dchrisum0lem2a  25206  mulogsumlem  25220  mulog2sumlem1  25223  mulog2sumlem2  25224  2vmadivsumlem  25229  selberg2lem  25239  selberg3lem1  25246  selberg4lem1  25249  pntrlog2bndlem3  25268  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntpbnd1  25275  pntlemc  25284  pntlemr  25291  pntlemk  25295  pntlemo  25296  abvcxp  25304  ostth2lem1  25307  padicabv  25319  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  ostth2  25326  legso  25494  trgcopy  25696  eucrct2eupth  27105  nvmtri  27526  imsmetlem  27545  vacn  27549  nmcvcn  27550  smcnlem  27552  blometi  27658  ipblnfi  27711  minvecolem2  27731  hhssnv  28121  nmcoplbi  28887  nmopcoi  28954  nmopcoadji  28960  idleop  28990  cdj1i  29292  isoun  29479  xlt2addrd  29523  omndmul  29714  ogrpsub  29717  archirngz  29743  gsumle  29779  ofldchr  29814  pstmxmet  29940  nexple  30071  esumpmono  30141  esumcvg  30148  meascnbl  30282  omsmon  30360  omsmeas  30385  dstfrvinc  30538  hgt750lemd  30726  hgt750lema  30735  hgt750leme  30736  derangenlem  31153  subfaclefac  31158  subfaclim  31170  erdszelem10  31182  sinccvglem  31566  iprodefisum  31627  noextendlt  31822  noextendgt  31823  nosupbnd1  31860  nosupbnd2lem1  31861  unbdqndv2lem2  32501  itg2gt0cn  33465  ibladdnclem  33466  iblabsnc  33474  iblmulc2nc  33475  itgabsnc  33479  bddiblnc  33480  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  mettrifi  33553  equivbnd2  33591  heiborlem6  33615  bfplem1  33621  bfp  33623  rrnmet  33628  rrndstprj1  33629  rrndstprj2  33630  dalawlem3  35159  dalawlem4  35160  dalawlem6  35162  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  dalawlem15  35171  cdleme3c  35517  cdleme7e  35534  cdleme26e  35647  cdleme26eALTN  35649  cdleme27a  35655  cdleme32c  35731  cdleme32e  35733  cdleme32le  35735  cdlemg9b  35921  cdlemg12b  35932  cdlemg12d  35934  trlcolem  36014  trlcone  36016  cdlemk7  36136  cdlemk7u  36158  cdlemk39  36204  cdlemk11ta  36217  cdlemk11tc  36233  mapdcnvatN  36955  irrapxlem5  37390  pell1qrge1  37434  pell1qrgaplem  37437  pell14qrgapw  37440  pellqrex  37443  pellfund14  37462  expmordi  37512  jm2.17a  37527  jm2.17c  37529  acongeq  37550  jm2.19  37560  jm2.27a  37572  jm2.27c  37574  jm3.1lem2  37585  areaquad  37802  rp-isfinite6  37864  hashnzfzclim  38521  binomcxplemnotnn0  38555  absimlere  39710  ltmod  39870  dvbdfbdioolem2  40144  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem3  40220  stoweidlem26  40243  wallispilem1  40282  wallispilem5  40286  stirlinglem1  40291  stirlinglem5  40295  stirlinglem8  40298  stirlinglem10  40300  stirlinglem12  40302  fourierdlem6  40330  fourierdlem7  40331  fourierdlem14  40338  fourierdlem19  40343  fourierdlem35  40359  fourierdlem39  40363  fourierdlem42  40366  fourierdlem50  40373  fourierdlem73  40396  fourierdlem76  40399  fourierdlem77  40400  fourierdlem81  40404  fourierdlem90  40413  fourierdlem92  40415  fourierdlem93  40416  fourierdlem111  40434  fouriersw  40448  etransclem38  40489  sge0split  40626  lighneallem4a  41525  rnghmsubcsetc  41977  rhmsubcsetc  42023  rhmsubcrngc  42029  rhmsubc  42090  rhmsubcALTV  42108  logbpw2m1  42361  dignn0flhalflem1  42409  dignn0flhalflem2  42410  amgmwlem  42548