Theorem breqtrrd 4681

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
breqtrrd.1	|- ( ph -> A R B )
breqtrrd.2	|- ( ph -> C = B )

Assertion

Ref	Expression
breqtrrd	|- ( ph -> A R C )

Proof of Theorem breqtrrd

Step	Hyp	Ref	Expression
1		breqtrrd.1	. 2 |- ( ph -> A R B )
2		breqtrrd.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2628	. 2 |- ( ph -> B = C )
4	1, 3	breqtrd 4679	1 |- ( ph -> A R C )

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:  marypha1lem  8339  marypha2  8345  unxpwdom  8494  uncdadom  8993  cdacomen  9003  cdaassen  9004  xpcdaen  9005  onacda  9019  infcdaabs  9028  cfss  9087  tskuni  9605  ltexnq  9797  lt2addmuld  11282  div4p1lem1div2  11287  mul2lt0rgt0  11933  xrmax1  12006  xrmax2  12007  max1ALT  12017  qbtwnxr  12031  xleadd1a  12083  xlt2add  12090  xlesubadd  12093  xmulgt0  12113  xlemul1a  12118  xov1plusxeqvd  12318  uzsubsubfz  12363  fzctr  12451  subfzo0  12590  flflp1  12608  fldiv4lem1div2uz2  12637  ceilge  12645  modge0  12678  modlt  12679  modid  12695  m1modge3gt1  12717  modaddmodup  12733  sermono  12833  seqf1olem1  12840  seqf1olem2  12841  leexp1a  12919  sqgt0  12932  sqge0  12940  nnlesq  12968  expnbnd  12993  expmulnbnd  12996  discr1  13000  facwordi  13076  faclbnd5  13085  nfile  13150  hashdom  13168  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  ccatws1n0  13409  swrds2  13685  cjmulge0  13886  resqrtcl  13994  absge0  14027  sqreulem  14099  amgm2  14109  rlimdm  14282  rlimge0  14312  reccn2  14327  climle  14370  climserle  14393  isercoll2  14399  iseraltlem1  14412  iseralt  14415  isumclim2  14489  isumclim3  14490  isumge0  14497  fsumless  14528  cvgcmp  14548  cvgcmpce  14550  abscvgcvg  14551  isumsup2  14578  isumltss  14580  climcndslem1  14581  climcnds  14583  supcvg  14588  harmonic  14591  expcnv  14596  explecnv  14597  cvgrat  14615  mertenslem1  14616  mertenslem2  14617  clim2div  14621  ntrivcvgtail  14632  iprodclim2  14730  iprodclim3  14731  efcvg  14815  ege2le3  14820  efaddlem  14823  eftlub  14839  effsumlt  14841  tanhlt1  14890  ef01bndlem  14914  sin02gt0  14922  rpnnen2lem4  14946  ruclem2  14961  ruclem3  14962  ruclem9  14967  iddvdsexp  15005  dvdsadd  15024  dvdsfac  15048  dvdsmod  15050  3dvds  15052  3dvdsOLD  15053  omoe  15088  sumeven  15110  divalglem1  15117  flodddiv4t2lthalf  15140  bitsfzo  15157  bitsmod  15158  bitscmp  15160  bitsinv1lem  15163  sadcaddlem  15179  sadadd3  15183  sadaddlem  15188  dvdssqim  15273  dvdsmulgcd  15274  nn0seqcvgd  15283  dvdslcm  15311  lcmgcdlem  15319  dvdslcmf  15344  lcmfunsnlem2lem2  15352  mulgcddvds  15369  qredeq  15371  cncongr2  15382  sqnprm  15414  isprm6  15426  nonsq  15467  hashdvds  15480  prmdiv  15490  odzdvds  15500  pythagtriplem4  15524  pcpre1  15547  pcdvdsb  15573  pcz  15585  pcprmpw2  15586  pcaddlem  15592  pcadd  15593  pcadd2  15594  pcmpt  15596  pcmptdvds  15598  fldivp1  15601  pcfaclem  15602  pockthlem  15609  prmreclem1  15620  prmreclem3  15622  prmreclem5  15624  prmreclem6  15625  4sqlem6  15647  4sqlem8  15649  4sqlem11  15659  4sqlem12  15660  4sqlem14  15662  4sqlem16  15664  vdwlem3  15687  vdwlem9  15693  vdwlem10  15694  vdwlem12  15696  ramub1lem2  15731  prmgap  15763  prmgaplcm  15764  prmgapprmo  15766  mreexexd  16308  invfuc  16634  ple1  17044  eqgen  17647  lagsubg  17656  pgpfi  18020  sylow2alem2  18033  sylow2a  18034  sylow3lem4  18045  efgsrel  18147  odadd1  18251  odadd2  18252  gexex  18256  lt6abl  18296  dprd2d2  18443  dmdprdpr  18448  ablfacrp2  18466  ablfac1c  18470  pgpfaclem1  18480  ablfac2  18488  dvdsrmul1  18653  unitmulclb  18665  subrguss  18795  abvres  18839  ply1coefsupp  19665  evl1gsumadd  19722  znfld  19909  znunit  19912  frlmisfrlm  20187  matgsum  20243  pm2mpcl  20602  psmetxrge0  22118  isxmet2d  22132  mettri  22157  xmettri3  22158  mettri3  22159  xmetrtri2  22161  prdsxmetlem  22173  imasdsf1olem  22178  xblss2ps  22206  blss2ps  22208  blss2  22209  blssps  22229  blss  22230  prdsbl  22296  dscmet  22377  nmge0  22421  nmmtri  22426  tngngp3  22460  nlmvscnlem2  22489  nrginvrcnlem  22495  nmoix  22533  nmoleub  22535  blcvx  22601  xrsxmet  22612  opnreen  22634  xrge0tsms  22637  icopnfcnv  22741  xrhmeo  22745  lebnumii  22765  pcophtb  22829  pi1grplem  22849  nmoleub2lem  22914  ipcau2  23033  tchcphlem1  23034  ipcau  23037  ipcnlem2  23043  rrxcph  23180  minveclem2  23197  minveclem3b  23199  pjthlem1  23208  pjthlem2  23209  ivthlem3  23222  ivth2  23224  ovolfsf  23240  ovolsslem  23252  ovollb2lem  23256  ovollb2  23257  ovolctb  23258  ovolfiniun  23269  ovolicc1  23284  ovolicc2lem4  23288  ovolicc2  23290  nulmbl2  23304  unmbl  23305  ioombl1lem4  23329  uniioombllem4  23354  uniioombllem6  23356  volivth  23375  vitalilem4  23380  itg1ge0  23453  itg1ge0a  23478  itg1lea  23479  itg1climres  23481  mbfi1fseqlem5  23486  itg2ub  23500  itg2seq  23509  itg2uba  23510  itg2splitlem  23515  itg2split  23516  itg2monolem3  23519  itg2mono  23520  itg2i1fseq2  23523  itg2addlem  23525  iblss  23571  itggt0  23608  dvferm2lem  23749  dvlip  23756  dvivthlem1  23771  dvfsumlem2  23790  dvfsumlem3  23791  ftc1lem4  23802  ply1divmo  23895  ply1remlem  23922  fta1glem2  23926  ig1pdvds  23936  plyeq0lem  23966  plydiveu  24053  fta1lem  24062  vieta1lem2  24066  aaliou3lem2  24098  aaliou3lem8  24100  ulmcn  24153  mtest  24158  itgulm  24162  radcnvlem1  24167  radcnvlt1  24172  dvradcnv  24175  pserdvlem2  24182  abelthlem2  24186  abelthlem6  24190  abelthlem7  24192  abelthlem9  24194  tangtx  24257  sinq12gt0  24259  sineq0  24273  cosordlem  24277  tanord  24284  tanregt0  24285  logrnaddcl  24321  logcj  24352  argregt0  24356  argrege0  24357  argimgt0  24358  argimlt0  24359  logimul  24360  logneg2  24361  logdivlti  24366  divlogrlim  24381  logcnlem3  24390  logcnlem4  24391  dvlog2lem  24398  logtayl  24406  rpcxpcl  24422  cxpsqrtlem  24448  cxpaddle  24493  isosctrlem1  24548  asinlem3a  24597  asinlem3  24598  asinneg  24613  asinsinlem  24618  asinsin  24619  atanlogaddlem  24640  atanlogadd  24641  atanlogsublem  24642  atanlogsub  24643  atantan  24650  atanbndlem  24652  atantayl  24664  leibpi  24669  birthdaylem3  24680  areaf  24688  cxploglim  24704  jensenlem2  24714  jensen  24715  logdiflbnd  24721  harmonicbnd4  24737  fsumharmonic  24738  zetacvg  24741  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamcvg2  24781  wilthlem2  24795  wilthimp  24798  ftalem1  24799  ftalem2  24800  ftalem5  24803  basellem6  24812  basellem8  24814  basellem9  24815  chtge0  24838  chtublem  24936  logexprlim  24950  perfectlem1  24954  bcmax  25003  bposlem1  25009  bposlem2  25010  bposlem6  25014  bposlem7  25015  lgsdilem2  25058  lgsqrlem4  25074  lgsquadlem1  25105  2lgsoddprmlem2  25134  2sqlem3  25145  2sqlem8  25151  2sqblem  25156  chebbnd1lem2  25159  chtppilimlem1  25162  chtppilim  25164  chto1ub  25165  vmadivsum  25171  rplogsumlem1  25173  rplogsumlem2  25174  dchrisum0lem1a  25175  rpvmasumlem  25176  dchrisumlem1  25178  dchrisumlem2  25179  dchrvmasumlem2  25187  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem3  25208  dchrisum0  25209  mudivsum  25219  mulogsumlem  25220  mulog2sumlem1  25223  mulog2sumlem2  25224  2vmadivsumlem  25229  chpdifbndlem1  25242  selberg3lem1  25246  selberg4lem1  25249  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem2  25280  pntibndlem3  25281  pntlemd  25283  pntlemc  25284  pntlemb  25286  pntlemg  25287  pntlemh  25288  pntlemr  25291  pntlemf  25294  pntlemo  25296  abvcxp  25304  ostth2lem1  25307  padicabv  25319  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  ostth2  25326  ostth3  25327  tgcgr4  25426  legso  25494  krippenlem  25585  midex  25629  oppperpex  25645  ttgcontlem1  25765  axpaschlem  25820  axcontlem8  25851  upgrex  25987  nbfusgrlevtxm1  26279  finsumvtxdgeven  26448  wwlksnextproplem3  26806  clwlkclwwlk2  26904  clwwlksndivn  26957  clwlksf1clwwlklem1  26965  ex-ind-dvds  27318  nvabs  27527  nmooge0  27622  nmoolb  27626  siii  27708  minvecolem2  27731  minvecolem4  27736  minvecolem5  27737  hlipgt0  27770  normge0  27983  normpyc  28003  pjhthlem1  28250  pjige0i  28549  nmoplb  28766  nmfnlb  28783  branmfn  28964  pjssdif2i  29033  stlei  29099  xlt2addrd  29523  eliccelico  29539  elicoelioo  29540  bcm1n  29554  fsumiunle  29575  2sqmod  29648  omndmul2  29712  archirngz  29743  archiabllem2c  29749  xrge0tsmsd  29785  ofldchr  29814  psgnfzto1stlem  29850  madjusmdetlem2  29894  locfinreflem  29907  xrge0iifiso  29981  nexple  30071  gsumesum  30121  esumcst  30125  esumpcvgval  30140  esumcvg  30148  esumiun  30156  measssd  30278  measunl  30279  omssubadd  30362  carsgclctunlem3  30382  pmeasmono  30386  sibfof  30402  oddpwdc  30416  eulerpartlemgc  30424  iwrdsplit  30449  ballotlemsgt1  30572  ballotlemsel1i  30574  sgnmul  30604  signsply0  30628  signstfvc  30651  signsvtp  30660  signsvfpn  30662  fdvposlt  30677  fdvneggt  30678  fdvnegge  30680  logdivsqrle  30728  hgt750lemf  30731  tgoldbachgtde  30738  subfaclim  31170  erdszelem7  31179  erdszelem8  31180  cvmliftlem2  31268  snmlff  31311  sinccvglem  31566  climlec3  31619  faclim  31632  dvdspw  31636  nodense  31842  nosupbnd2lem1  31861  noetalem2  31864  fnejoin1  32363  poimirlem12  33421  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  poimirlem28  33437  broucube  33443  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnclem  33461  itg2addnclem3  33463  itg2gt0cn  33465  itggt0cn  33482  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  isbnd3  33583  ssbnd  33587  heiborlem8  33617  bfplem2  33622  rrncmslem  33631  rrnequiv  33634  rrntotbnd  33635  lcv1  34328  lsatcv0eq  34334  lsatcvat3  34339  cvlsupr2  34630  hlatlej2  34662  cvrval4N  34700  cvratlem  34707  atcvr0eq  34712  2atlt  34725  atbtwnex  34734  athgt  34742  1cvrat  34762  ps-1  34763  hlatexch3N  34766  hlatexch4  34767  3atlem2  34770  atcvrlln2  34805  lplnexllnN  34850  4atlem3a  34883  4atlem10b  34891  4atlem11b  34894  4atlem12b  34897  2lplnja  34905  dalemply  34940  dalemsly  34941  dalem1  34945  dalem6  34954  dalem7  34955  dalem-cly  34957  dalem11  34960  dalem12  34961  dalem16  34965  dalem17  34966  dalem38  34996  dalem44  35002  dalem61  35019  lnatexN  35065  lncvrat  35068  lncmp  35069  paddasslem2  35107  dalawlem3  35159  dalawlem6  35162  dalawlem11  35167  lhpmcvr  35309  lhp2atne  35320  lhp2at0ne  35322  lautj  35379  trlval4  35475  cdlemc2  35479  cdlemc5  35482  cdleme3b  35516  cdleme11c  35548  cdleme19a  35591  cdleme20j  35606  cdleme22f  35634  cdleme23c  35639  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme35fnpq  35737  cdleme48bw  35790  cdlemg10a  35928  cdlemg11b  35930  cdlemg17g  35955  cdlemg18c  35968  cdlemi1  36106  cdlemk52  36242  dia2dimlem1  36353  dihord1  36507  dihjatcclem4  36710  eldioph2lem1  37323  lzenom  37333  irrapxlem1  37386  irrapxlem4  37389  irrapxlem5  37390  pell14qrgt0  37423  pell1qrge1  37434  pell1qrgap  37438  pellfundge  37446  pellfundex  37450  pellfund14  37462  rmspecsqrtnq  37470  rmspecsqrtnqOLD  37471  rmxypos  37514  ltrmynn0  37515  ltrmxnn0  37516  jm2.24nn  37526  jm2.17b  37528  jm2.17c  37529  jm2.24  37530  congadd  37533  congsym  37535  congneg  37536  congid  37538  mzpcong  37539  acongrep  37547  acongeq  37550  jm2.18  37555  jm2.19  37560  jm2.23  37563  jm2.25  37566  jm2.26lem3  37568  jm2.15nn0  37570  jm2.16nn0  37571  jm2.27a  37572  jm2.27c  37574  jm3.1lem1  37584  idomrootle  37773  idomsubgmo  37776  inductionexd  38453  imo72b2  38475  dvgrat  38511  radcnvrat  38513  binomcxplemnn0  38548  binomcxplemnotnn0  38555  cncmpmax  39191  rnmptlb  39453  zltlesub  39497  infxrpnf  39674  fmul01  39812  fmul01lt1lem1  39816  climdivf  39844  sumnnodd  39862  climinf2lem  39938  limsup10exlem  40004  climliminf  40038  dfxlim2v  40073  dvdivbd  40138  volge0  40177  stoweidlem1  40218  stoweidlem16  40233  stoweidlem18  40235  stoweidlem24  40241  stoweidlem26  40243  stoweidlem36  40253  stoweidlem38  40255  stoweidlem41  40258  stoweidlem42  40259  stoweidlem44  40261  stoweidlem45  40262  stoweidlem48  40265  stoweidlem62  40279  wallispilem5  40286  stirlinglem1  40291  stirlinglem5  40295  stirlinglem7  40297  stirlinglem8  40298  stirlinglem9  40299  stirlinglem11  40301  fourierdlem4  40328  fourierdlem10  40334  fourierdlem37  40361  fourierdlem47  40370  fourierdlem72  40395  fourierdlem74  40397  fourierdlem79  40402  fourierdlem82  40405  fourierdlem89  40412  fourierdlem91  40414  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  etransclem24  40475  etransclem25  40476  etransclem28  40479  etransclem37  40488  etransclem38  40489  etransclem44  40495  vonicclem1  40897  pimconstlt0  40914  smfsuplem1  41017  rlimdmafv  41257  2elfz2melfz  41328  iccpartgtprec  41356  iccpartlt  41360  iccpartgtl  41362  sqrtpwpw2p  41450  fmtnodvds  41456  goldbachthlem1  41457  lighneallem4a  41525  perfectALTVlem1  41630  cznnring  41956  rhmsubcrngc  42029  altgsumbcALT  42131  expnegico01  42308  flnn0div2ge  42327  rege1logbrege0  42352  fllogbd  42354  fllog2  42362  nnpw2blen  42374  nnolog2flm1  42384  dignn0ldlem  42396  dignn0flhalflem1  42409  dignn0flhalflem2  42410