Theorem breqtrrd 4121

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

Syntax hints:   -> wi 4   = wceq 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  frirrg  4453  fidcen  7131  unsnfidcex  7155  unsnfidcel  7156  addlocprlemeq  7796  ltexprlemopl  7864  recexprlemloc  7894  cauappcvgprlemopl  7909  cauappcvgprlemladdfu  7917  cauappcvgprlem1  7922  caucvgprlemopl  7932  caucvgprlemladdfu  7940  caucvgprprlemopl  7960  caucvgprprlemexbt  7969  mulgt0sr  8041  archsr  8045  caucvgsrlemoffgt1  8062  suplocsrlemb  8069  suplocsrlem  8071  mulap0r  8837  prodgt0  9074  div4p1lem1div2  9440  mul2lt0rgt0  10039  xnn0dcle  10081  xnn0letri  10082  xleadd1a  10152  xltadd1  10155  xlt2add  10159  xposdif  10161  xlesubadd  10162  xleaddadd  10166  uzsubsubfz  10327  fzctr  10413  subfzo0  10534  exbtwnzlemstep  10553  exbtwnzlemex  10555  rebtwn2zlemstep  10558  rebtwn2z  10560  qbtwnxr  10563  xqltnle  10573  fldiv4lem1div2uz2  10612  ceilqge  10618  modqge0  10640  modqlt  10641  modqid  10657  m1modge3gt1  10679  modaddmodup  10695  addmodlteq  10706  ser3mono  10795  seqf1oglem1  10827  seqf1oglem2  10828  ser3ge0  10844  ser3le  10845  leexp1a  10902  sqgt0ap  10916  sqge0  10924  nnlesq  10951  expnbnd  10971  nn0opthlem2d  11029  facwordi  11048  filtinf  11099  hashunlem  11113  zfz1isolemiso  11149  cats1fvd  11396  cjmulge0  11512  resqrexlemover  11633  resqrexlemdec  11634  resqrexlemlo  11636  resqrexlemcalc3  11639  resqrexlemcvg  11642  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemga  11646  absge0  11683  amgm2  11741  maxle1  11834  bdtrilem  11862  xrmaxifle  11869  xrmaxiflemlub  11871  xrmaxiflemval  11873  xrmax1sup  11876  xrmaxltsup  11881  xrmaxadd  11884  xrbdtri  11899  reccn2ap  11936  climle  11957  climserle  11968  isumclim2  12046  isumclim3  12047  isumge0  12054  fsumlessfi  12084  expcnvap0  12126  expcnvre  12127  explecnv  12129  absltap  12133  cvgratnnlembern  12147  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratnnlemabsle  12151  cvgratnnlemfm  12153  cvgratnnlemrate  12154  mertenslemi1  12159  mertenslem2  12160  clim2divap  12164  prodmodclem3  12199  efcvg  12290  ege2le3  12295  efaddlem  12298  eftlub  12314  effsumlt  12316  ef01bndlem  12380  sin02gt0  12388  eirrap  12402  iddvdsexp  12439  dvdsadd  12460  dvdsfac  12484  dvdsmod  12486  3dvds  12488  omoe  12520  divalglemnn  12542  divalglemnqt  12544  flodddiv4t2lthalf  12563  bitsfzo  12579  bitsmod  12580  bitscmp  12582  bitsinv1lem  12585  dvdslegcd  12598  dfgcd3  12644  dvdssqim  12658  dvdsmulgcd  12659  nn0seqcvgd  12676  dvdslcm  12704  lcmgcdlem  12712  mulgcddvds  12729  qredeq  12731  cncongr2  12739  sqnprm  12771  isprm6  12782  sqpweven  12810  znege1  12813  sqrt2irrap  12815  nonsq  12842  hashdvds  12856  prmdiv  12870  odzdvds  12881  pythagtriplem4  12904  pcpre1  12928  pcdvdsb  12956  pcz  12968  pcprmpw2  12969  pcaddlem  12975  pcadd  12976  pcadd2  12977  pcmpt  12979  pcmptdvds  12981  fldivp1  12984  pcfaclem  12985  pockthlem  12992  4sqlem6  13019  4sqlem8  13021  4sqexercise1  13034  4sqexercise2  13035  4sqlemsdc  13036  4sqlem11  13037  4sqlem12  13038  4sqlem14  13040  4sqlem16  13042  ennnfonelemkh  13096  nninfdclemp1  13134  eqgen  13877  dvdsrmul1  14180  unitmulclb  14192  subrguss  14314  znidom  14736  znunit  14738  mplsubgfilemcl  14783  psmetxrge0  15126  isxmet2d  15142  mettri  15167  xmettri3  15168  mettri3  15169  xblss2ps  15198  blss2ps  15200  blss2  15201  blssps  15221  blss  15222  xmetxp  15301  ivthdec  15438  ivthreinc  15439  hoverb  15442  hovergt0  15444  sin0pilem1  15575  sinq12gt0  15624  tangtx  15632  cosordlem  15643  cosq34lt1  15644  logdivlti  15675  logbgcd1irrap  15764  perfectlem1  15796  lgsdilem2  15838  gausslemma2dlem1f1o  15862  lgsquadlem1  15879  2lgsoddprmlem2  15908  2sqlem3  15919  2sqlem8  15925  usgrsizedgen  16137  cvgcmp2nlemabs  16747  trilpolemclim  16751  trilpolemeq1  16755  apdifflemf  16761  apdifflemr  16762  nconstwlpolemgt0  16780