Theorem breqtrrd 4058

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031

This theorem is referenced by:  frirrg  4382  unsnfidcex  6978  unsnfidcel  6979  addlocprlemeq  7595  ltexprlemopl  7663  recexprlemloc  7693  cauappcvgprlemopl  7708  cauappcvgprlemladdfu  7716  cauappcvgprlem1  7721  caucvgprlemopl  7731  caucvgprlemladdfu  7739  caucvgprprlemopl  7759  caucvgprprlemexbt  7768  mulgt0sr  7840  archsr  7844  caucvgsrlemoffgt1  7861  suplocsrlemb  7868  suplocsrlem  7870  mulap0r  8636  prodgt0  8873  div4p1lem1div2  9239  mul2lt0rgt0  9829  xnn0dcle  9871  xnn0letri  9872  xleadd1a  9942  xltadd1  9945  xlt2add  9949  xposdif  9951  xlesubadd  9952  xleaddadd  9956  uzsubsubfz  10116  fzctr  10202  subfzo0  10312  exbtwnzlemstep  10319  exbtwnzlemex  10321  rebtwn2zlemstep  10324  rebtwn2z  10326  qbtwnxr  10329  xqltnle  10339  fldiv4lem1div2uz2  10378  ceilqge  10384  modqge0  10406  modqlt  10407  modqid  10423  m1modge3gt1  10445  modaddmodup  10461  addmodlteq  10472  ser3mono  10561  seqf1oglem1  10593  seqf1oglem2  10594  ser3ge0  10610  ser3le  10611  leexp1a  10668  sqgt0ap  10682  sqge0  10690  nnlesq  10717  expnbnd  10737  nn0opthlem2d  10795  facwordi  10814  filtinf  10865  hashunlem  10878  zfz1isolemiso  10913  cjmulge0  11036  resqrexlemover  11157  resqrexlemdec  11158  resqrexlemlo  11160  resqrexlemcalc3  11163  resqrexlemcvg  11166  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemga  11170  absge0  11207  amgm2  11265  maxle1  11358  bdtrilem  11385  xrmaxifle  11392  xrmaxiflemlub  11394  xrmaxiflemval  11396  xrmax1sup  11399  xrmaxltsup  11404  xrmaxadd  11407  xrbdtri  11422  reccn2ap  11459  climle  11480  climserle  11491  isumclim2  11568  isumclim3  11569  isumge0  11576  fsumlessfi  11606  expcnvap0  11648  expcnvre  11649  explecnv  11651  absltap  11655  cvgratnnlembern  11669  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  cvgratnnlemabsle  11673  cvgratnnlemfm  11675  cvgratnnlemrate  11676  mertenslemi1  11681  mertenslem2  11682  clim2divap  11686  prodmodclem3  11721  efcvg  11812  ege2le3  11817  efaddlem  11820  eftlub  11836  effsumlt  11838  ef01bndlem  11902  sin02gt0  11910  eirrap  11924  iddvdsexp  11961  dvdsadd  11982  dvdsfac  12005  dvdsmod  12007  omoe  12040  divalglemnn  12062  divalglemnqt  12064  flodddiv4t2lthalf  12081  dvdslegcd  12104  dfgcd3  12150  dvdssqim  12164  dvdsmulgcd  12165  nn0seqcvgd  12182  dvdslcm  12210  lcmgcdlem  12218  mulgcddvds  12235  qredeq  12237  cncongr2  12245  sqnprm  12277  isprm6  12288  sqpweven  12316  znege1  12319  sqrt2irrap  12321  nonsq  12348  hashdvds  12362  prmdiv  12376  odzdvds  12386  pythagtriplem4  12409  pcpre1  12433  pcdvdsb  12461  pcz  12473  pcprmpw2  12474  pcaddlem  12480  pcadd  12481  pcadd2  12482  pcmpt  12484  pcmptdvds  12486  fldivp1  12489  pcfaclem  12490  pockthlem  12497  4sqlem6  12524  4sqlem8  12526  4sqexercise1  12539  4sqexercise2  12540  4sqlemsdc  12541  4sqlem11  12542  4sqlem12  12543  4sqlem14  12545  4sqlem16  12547  ennnfonelemkh  12572  nninfdclemp1  12610  eqgen  13300  dvdsrmul1  13601  unitmulclb  13613  subrguss  13735  znidom  14156  znunit  14158  psmetxrge0  14511  isxmet2d  14527  mettri  14552  xmettri3  14553  mettri3  14554  xblss2ps  14583  blss2ps  14585  blss2  14586  blssps  14606  blss  14607  xmetxp  14686  ivthdec  14823  ivthreinc  14824  hoverb  14827  hovergt0  14829  sin0pilem1  14957  sinq12gt0  15006  tangtx  15014  cosordlem  15025  cosq34lt1  15026  logdivlti  15057  logbgcd1irrap  15143  lgsdilem2  15193  gausslemma2dlem1f1o  15217  lgsquadlem1  15234  2lgsoddprmlem2  15263  2sqlem3  15274  2sqlem8  15280  cvgcmp2nlemabs  15592  trilpolemclim  15596  trilpolemeq1  15600  apdifflemf  15606  apdifflemr  15607  nconstwlpolemgt0  15624