Theorem breqtrrd 4017

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 4015	1 |- ( ph -> A R C )

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

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 3589  df-pr 3590  df-op 3592  df-br 3990

This theorem is referenced by:  frirrg  4335  unsnfidcex  6897  unsnfidcel  6898  addlocprlemeq  7495  ltexprlemopl  7563  recexprlemloc  7593  cauappcvgprlemopl  7608  cauappcvgprlemladdfu  7616  cauappcvgprlem1  7621  caucvgprlemopl  7631  caucvgprlemladdfu  7639  caucvgprprlemopl  7659  caucvgprprlemexbt  7668  mulgt0sr  7740  archsr  7744  caucvgsrlemoffgt1  7761  suplocsrlemb  7768  suplocsrlem  7770  mulap0r  8534  prodgt0  8768  div4p1lem1div2  9131  mul2lt0rgt0  9717  xnn0dcle  9759  xnn0letri  9760  xleadd1a  9830  xltadd1  9833  xlt2add  9837  xposdif  9839  xlesubadd  9840  xleaddadd  9844  uzsubsubfz  10003  fzctr  10089  subfzo0  10198  exbtwnzlemstep  10204  exbtwnzlemex  10206  rebtwn2zlemstep  10209  rebtwn2z  10211  qbtwnxr  10214  ceilqge  10266  modqge0  10288  modqlt  10289  modqid  10305  m1modge3gt1  10327  modaddmodup  10343  addmodlteq  10354  ser3mono  10434  ser3ge0  10473  ser3le  10474  leexp1a  10531  sqgt0ap  10544  sqge0  10552  nnlesq  10579  expnbnd  10599  nn0opthlem2d  10655  facwordi  10674  filtinf  10726  hashunlem  10739  zfz1isolemiso  10774  cjmulge0  10853  resqrexlemover  10974  resqrexlemdec  10975  resqrexlemlo  10977  resqrexlemcalc3  10980  resqrexlemcvg  10983  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemga  10987  absge0  11024  amgm2  11082  maxle1  11175  bdtrilem  11202  xrmaxifle  11209  xrmaxiflemlub  11211  xrmaxiflemval  11213  xrmax1sup  11216  xrmaxltsup  11221  xrmaxadd  11224  xrbdtri  11239  reccn2ap  11276  climle  11297  climserle  11308  isumclim2  11385  isumclim3  11386  isumge0  11393  fsumlessfi  11423  expcnvap0  11465  expcnvre  11466  explecnv  11468  absltap  11472  cvgratnnlembern  11486  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemabsle  11490  cvgratnnlemfm  11492  cvgratnnlemrate  11493  mertenslemi1  11498  mertenslem2  11499  clim2divap  11503  prodmodclem3  11538  efcvg  11629  ege2le3  11634  efaddlem  11637  eftlub  11653  effsumlt  11655  ef01bndlem  11719  sin02gt0  11726  eirrap  11740  iddvdsexp  11777  dvdsadd  11798  dvdsfac  11820  dvdsmod  11822  omoe  11855  divalglemnn  11877  divalglemnqt  11879  flodddiv4t2lthalf  11896  dvdslegcd  11919  dfgcd3  11965  dvdssqim  11979  dvdsmulgcd  11980  nn0seqcvgd  11995  dvdslcm  12023  lcmgcdlem  12031  mulgcddvds  12048  qredeq  12050  cncongr2  12058  sqnprm  12090  isprm6  12101  sqpweven  12129  znege1  12132  sqrt2irrap  12134  nonsq  12161  hashdvds  12175  prmdiv  12189  odzdvds  12199  pythagtriplem4  12222  pcpre1  12246  pcdvdsb  12273  pcz  12285  pcprmpw2  12286  pcaddlem  12292  pcadd  12293  pcmpt  12295  pcmptdvds  12297  fldivp1  12300  pcfaclem  12301  pockthlem  12308  4sqlem6  12335  4sqlem8  12337  ennnfonelemkh  12367  nninfdclemp1  12405  psmetxrge0  13126  isxmet2d  13142  mettri  13167  xmettri3  13168  mettri3  13169  xblss2ps  13198  blss2ps  13200  blss2  13201  blssps  13221  blss  13222  xmetxp  13301  ivthdec  13416  sin0pilem1  13496  sinq12gt0  13545  tangtx  13553  cosordlem  13564  cosq34lt1  13565  logdivlti  13596  logbgcd1irrap  13682  lgsdilem2  13731  2sqlem3  13747  2sqlem8  13753  cvgcmp2nlemabs  14064  trilpolemclim  14068  trilpolemeq1  14072  apdifflemf  14078  apdifflemr  14079  nconstwlpolemgt0  14095