Theorem breqtrrd 4009

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

Syntax hints:   -> wi 4   = wceq 1343   class class class wbr 3981

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-br 3982

This theorem is referenced by:  frirrg  4327  unsnfidcex  6881  unsnfidcel  6882  addlocprlemeq  7470  ltexprlemopl  7538  recexprlemloc  7568  cauappcvgprlemopl  7583  cauappcvgprlemladdfu  7591  cauappcvgprlem1  7596  caucvgprlemopl  7606  caucvgprlemladdfu  7614  caucvgprprlemopl  7634  caucvgprprlemexbt  7643  mulgt0sr  7715  archsr  7719  caucvgsrlemoffgt1  7736  suplocsrlemb  7743  suplocsrlem  7745  mulap0r  8509  prodgt0  8743  div4p1lem1div2  9106  mul2lt0rgt0  9692  xnn0dcle  9734  xnn0letri  9735  xleadd1a  9805  xltadd1  9808  xlt2add  9812  xposdif  9814  xlesubadd  9815  xleaddadd  9819  uzsubsubfz  9978  fzctr  10064  subfzo0  10173  exbtwnzlemstep  10179  exbtwnzlemex  10181  rebtwn2zlemstep  10184  rebtwn2z  10186  qbtwnxr  10189  ceilqge  10241  modqge0  10263  modqlt  10264  modqid  10280  m1modge3gt1  10302  modaddmodup  10318  addmodlteq  10329  ser3mono  10409  ser3ge0  10448  ser3le  10449  leexp1a  10506  sqgt0ap  10519  sqge0  10527  nnlesq  10554  expnbnd  10574  nn0opthlem2d  10630  facwordi  10649  filtinf  10701  hashunlem  10713  zfz1isolemiso  10748  cjmulge0  10827  resqrexlemover  10948  resqrexlemdec  10949  resqrexlemlo  10951  resqrexlemcalc3  10954  resqrexlemcvg  10957  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemga  10961  absge0  10998  amgm2  11056  maxle1  11149  bdtrilem  11176  xrmaxifle  11183  xrmaxiflemlub  11185  xrmaxiflemval  11187  xrmax1sup  11190  xrmaxltsup  11195  xrmaxadd  11198  xrbdtri  11213  reccn2ap  11250  climle  11271  climserle  11282  isumclim2  11359  isumclim3  11360  isumge0  11367  fsumlessfi  11397  expcnvap0  11439  expcnvre  11440  explecnv  11442  absltap  11446  cvgratnnlembern  11460  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratnnlemabsle  11464  cvgratnnlemfm  11466  cvgratnnlemrate  11467  mertenslemi1  11472  mertenslem2  11473  clim2divap  11477  prodmodclem3  11512  efcvg  11603  ege2le3  11608  efaddlem  11611  eftlub  11627  effsumlt  11629  ef01bndlem  11693  sin02gt0  11700  eirrap  11714  iddvdsexp  11751  dvdsadd  11772  dvdsfac  11794  dvdsmod  11796  omoe  11829  divalglemnn  11851  divalglemnqt  11853  flodddiv4t2lthalf  11870  dvdslegcd  11893  dfgcd3  11939  dvdssqim  11953  dvdsmulgcd  11954  nn0seqcvgd  11969  dvdslcm  11997  lcmgcdlem  12005  mulgcddvds  12022  qredeq  12024  cncongr2  12032  sqnprm  12064  isprm6  12075  sqpweven  12103  znege1  12106  sqrt2irrap  12108  nonsq  12135  hashdvds  12149  prmdiv  12163  odzdvds  12173  pythagtriplem4  12196  pcpre1  12220  pcdvdsb  12247  pcz  12259  pcprmpw2  12260  pcaddlem  12266  pcadd  12267  pcmpt  12269  pcmptdvds  12271  fldivp1  12274  pcfaclem  12275  pockthlem  12282  4sqlem6  12309  4sqlem8  12311  ennnfonelemkh  12341  nninfdclemp1  12379  psmetxrge0  12932  isxmet2d  12948  mettri  12973  xmettri3  12974  mettri3  12975  xblss2ps  13004  blss2ps  13006  blss2  13007  blssps  13027  blss  13028  xmetxp  13107  ivthdec  13222  sin0pilem1  13302  sinq12gt0  13351  tangtx  13359  cosordlem  13370  cosq34lt1  13371  logdivlti  13402  logbgcd1irrap  13488  lgsdilem2  13537  2sqlem3  13553  2sqlem8  13559  cvgcmp2nlemabs  13871  trilpolemclim  13875  trilpolemeq1  13879  apdifflemf  13885  apdifflemr  13886  nconstwlpolemgt0  13902