Theorem breqtrrd 4015

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

Syntax hints:   -> wi 4   = wceq 1348   class class class wbr 3987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-br 3988

This theorem is referenced by:  frirrg  4333  unsnfidcex  6893  unsnfidcel  6894  addlocprlemeq  7482  ltexprlemopl  7550  recexprlemloc  7580  cauappcvgprlemopl  7595  cauappcvgprlemladdfu  7603  cauappcvgprlem1  7608  caucvgprlemopl  7618  caucvgprlemladdfu  7626  caucvgprprlemopl  7646  caucvgprprlemexbt  7655  mulgt0sr  7727  archsr  7731  caucvgsrlemoffgt1  7748  suplocsrlemb  7755  suplocsrlem  7757  mulap0r  8521  prodgt0  8755  div4p1lem1div2  9118  mul2lt0rgt0  9704  xnn0dcle  9746  xnn0letri  9747  xleadd1a  9817  xltadd1  9820  xlt2add  9824  xposdif  9826  xlesubadd  9827  xleaddadd  9831  uzsubsubfz  9990  fzctr  10076  subfzo0  10185  exbtwnzlemstep  10191  exbtwnzlemex  10193  rebtwn2zlemstep  10196  rebtwn2z  10198  qbtwnxr  10201  ceilqge  10253  modqge0  10275  modqlt  10276  modqid  10292  m1modge3gt1  10314  modaddmodup  10330  addmodlteq  10341  ser3mono  10421  ser3ge0  10460  ser3le  10461  leexp1a  10518  sqgt0ap  10531  sqge0  10539  nnlesq  10566  expnbnd  10586  nn0opthlem2d  10642  facwordi  10661  filtinf  10713  hashunlem  10726  zfz1isolemiso  10761  cjmulge0  10840  resqrexlemover  10961  resqrexlemdec  10962  resqrexlemlo  10964  resqrexlemcalc3  10967  resqrexlemcvg  10970  resqrexlemoverl  10972  resqrexlemglsq  10973  resqrexlemga  10974  absge0  11011  amgm2  11069  maxle1  11162  bdtrilem  11189  xrmaxifle  11196  xrmaxiflemlub  11198  xrmaxiflemval  11200  xrmax1sup  11203  xrmaxltsup  11208  xrmaxadd  11211  xrbdtri  11226  reccn2ap  11263  climle  11284  climserle  11295  isumclim2  11372  isumclim3  11373  isumge0  11380  fsumlessfi  11410  expcnvap0  11452  expcnvre  11453  explecnv  11455  absltap  11459  cvgratnnlembern  11473  cvgratnnlemnexp  11474  cvgratnnlemmn  11475  cvgratnnlemabsle  11477  cvgratnnlemfm  11479  cvgratnnlemrate  11480  mertenslemi1  11485  mertenslem2  11486  clim2divap  11490  prodmodclem3  11525  efcvg  11616  ege2le3  11621  efaddlem  11624  eftlub  11640  effsumlt  11642  ef01bndlem  11706  sin02gt0  11713  eirrap  11727  iddvdsexp  11764  dvdsadd  11785  dvdsfac  11807  dvdsmod  11809  omoe  11842  divalglemnn  11864  divalglemnqt  11866  flodddiv4t2lthalf  11883  dvdslegcd  11906  dfgcd3  11952  dvdssqim  11966  dvdsmulgcd  11967  nn0seqcvgd  11982  dvdslcm  12010  lcmgcdlem  12018  mulgcddvds  12035  qredeq  12037  cncongr2  12045  sqnprm  12077  isprm6  12088  sqpweven  12116  znege1  12119  sqrt2irrap  12121  nonsq  12148  hashdvds  12162  prmdiv  12176  odzdvds  12186  pythagtriplem4  12209  pcpre1  12233  pcdvdsb  12260  pcz  12272  pcprmpw2  12273  pcaddlem  12279  pcadd  12280  pcmpt  12282  pcmptdvds  12284  fldivp1  12287  pcfaclem  12288  pockthlem  12295  4sqlem6  12322  4sqlem8  12324  ennnfonelemkh  12354  nninfdclemp1  12392  psmetxrge0  13047  isxmet2d  13063  mettri  13088  xmettri3  13089  mettri3  13090  xblss2ps  13119  blss2ps  13121  blss2  13122  blssps  13142  blss  13143  xmetxp  13222  ivthdec  13337  sin0pilem1  13417  sinq12gt0  13466  tangtx  13474  cosordlem  13485  cosq34lt1  13486  logdivlti  13517  logbgcd1irrap  13603  lgsdilem2  13652  2sqlem3  13668  2sqlem8  13674  cvgcmp2nlemabs  13986  trilpolemclim  13990  trilpolemeq1  13994  apdifflemf  14000  apdifflemr  14001  nconstwlpolemgt0  14017