Theorem breqtrrd 4062

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 2202	. 2 |- ( ph -> B = C )
4	1, 3	breqtrd 4060	1 |- ( ph -> A R C )

Syntax hints:   -> wi 4   = wceq 1364   class class class wbr 4034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  frirrg  4386  unsnfidcex  6990  unsnfidcel  6991  addlocprlemeq  7617  ltexprlemopl  7685  recexprlemloc  7715  cauappcvgprlemopl  7730  cauappcvgprlemladdfu  7738  cauappcvgprlem1  7743  caucvgprlemopl  7753  caucvgprlemladdfu  7761  caucvgprprlemopl  7781  caucvgprprlemexbt  7790  mulgt0sr  7862  archsr  7866  caucvgsrlemoffgt1  7883  suplocsrlemb  7890  suplocsrlem  7892  mulap0r  8659  prodgt0  8896  div4p1lem1div2  9262  mul2lt0rgt0  9852  xnn0dcle  9894  xnn0letri  9895  xleadd1a  9965  xltadd1  9968  xlt2add  9972  xposdif  9974  xlesubadd  9975  xleaddadd  9979  uzsubsubfz  10139  fzctr  10225  subfzo0  10335  exbtwnzlemstep  10354  exbtwnzlemex  10356  rebtwn2zlemstep  10359  rebtwn2z  10361  qbtwnxr  10364  xqltnle  10374  fldiv4lem1div2uz2  10413  ceilqge  10419  modqge0  10441  modqlt  10442  modqid  10458  m1modge3gt1  10480  modaddmodup  10496  addmodlteq  10507  ser3mono  10596  seqf1oglem1  10628  seqf1oglem2  10629  ser3ge0  10645  ser3le  10646  leexp1a  10703  sqgt0ap  10717  sqge0  10725  nnlesq  10752  expnbnd  10772  nn0opthlem2d  10830  facwordi  10849  filtinf  10900  hashunlem  10913  zfz1isolemiso  10948  cjmulge0  11071  resqrexlemover  11192  resqrexlemdec  11193  resqrexlemlo  11195  resqrexlemcalc3  11198  resqrexlemcvg  11201  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemga  11205  absge0  11242  amgm2  11300  maxle1  11393  bdtrilem  11421  xrmaxifle  11428  xrmaxiflemlub  11430  xrmaxiflemval  11432  xrmax1sup  11435  xrmaxltsup  11440  xrmaxadd  11443  xrbdtri  11458  reccn2ap  11495  climle  11516  climserle  11527  isumclim2  11604  isumclim3  11605  isumge0  11612  fsumlessfi  11642  expcnvap0  11684  expcnvre  11685  explecnv  11687  absltap  11691  cvgratnnlembern  11705  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemabsle  11709  cvgratnnlemfm  11711  cvgratnnlemrate  11712  mertenslemi1  11717  mertenslem2  11718  clim2divap  11722  prodmodclem3  11757  efcvg  11848  ege2le3  11853  efaddlem  11856  eftlub  11872  effsumlt  11874  ef01bndlem  11938  sin02gt0  11946  eirrap  11960  iddvdsexp  11997  dvdsadd  12018  dvdsfac  12042  dvdsmod  12044  3dvds  12046  omoe  12078  divalglemnn  12100  divalglemnqt  12102  flodddiv4t2lthalf  12121  bitsfzo  12137  bitsmod  12138  bitscmp  12140  bitsinv1lem  12143  dvdslegcd  12156  dfgcd3  12202  dvdssqim  12216  dvdsmulgcd  12217  nn0seqcvgd  12234  dvdslcm  12262  lcmgcdlem  12270  mulgcddvds  12287  qredeq  12289  cncongr2  12297  sqnprm  12329  isprm6  12340  sqpweven  12368  znege1  12371  sqrt2irrap  12373  nonsq  12400  hashdvds  12414  prmdiv  12428  odzdvds  12439  pythagtriplem4  12462  pcpre1  12486  pcdvdsb  12514  pcz  12526  pcprmpw2  12527  pcaddlem  12533  pcadd  12534  pcadd2  12535  pcmpt  12537  pcmptdvds  12539  fldivp1  12542  pcfaclem  12543  pockthlem  12550  4sqlem6  12577  4sqlem8  12579  4sqexercise1  12592  4sqexercise2  12593  4sqlemsdc  12594  4sqlem11  12595  4sqlem12  12596  4sqlem14  12598  4sqlem16  12600  ennnfonelemkh  12654  nninfdclemp1  12692  eqgen  13433  dvdsrmul1  13734  unitmulclb  13746  subrguss  13868  znidom  14289  znunit  14291  psmetxrge0  14652  isxmet2d  14668  mettri  14693  xmettri3  14694  mettri3  14695  xblss2ps  14724  blss2ps  14726  blss2  14727  blssps  14747  blss  14748  xmetxp  14827  ivthdec  14964  ivthreinc  14965  hoverb  14968  hovergt0  14970  sin0pilem1  15101  sinq12gt0  15150  tangtx  15158  cosordlem  15169  cosq34lt1  15170  logdivlti  15201  logbgcd1irrap  15290  perfectlem1  15319  lgsdilem2  15361  gausslemma2dlem1f1o  15385  lgsquadlem1  15402  2lgsoddprmlem2  15431  2sqlem3  15442  2sqlem8  15448  cvgcmp2nlemabs  15763  trilpolemclim  15767  trilpolemeq1  15771  apdifflemf  15777  apdifflemr  15778  nconstwlpolemgt0  15795