Theorem breqtrrd 4062

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035

This theorem is referenced by:  frirrg  4386  unsnfidcex  6982  unsnfidcel  6983  addlocprlemeq  7602  ltexprlemopl  7670  recexprlemloc  7700  cauappcvgprlemopl  7715  cauappcvgprlemladdfu  7723  cauappcvgprlem1  7728  caucvgprlemopl  7738  caucvgprlemladdfu  7746  caucvgprprlemopl  7766  caucvgprprlemexbt  7775  mulgt0sr  7847  archsr  7851  caucvgsrlemoffgt1  7868  suplocsrlemb  7875  suplocsrlem  7877  mulap0r  8644  prodgt0  8881  div4p1lem1div2  9247  mul2lt0rgt0  9837  xnn0dcle  9879  xnn0letri  9880  xleadd1a  9950  xltadd1  9953  xlt2add  9957  xposdif  9959  xlesubadd  9960  xleaddadd  9964  uzsubsubfz  10124  fzctr  10210  subfzo0  10320  exbtwnzlemstep  10339  exbtwnzlemex  10341  rebtwn2zlemstep  10344  rebtwn2z  10346  qbtwnxr  10349  xqltnle  10359  fldiv4lem1div2uz2  10398  ceilqge  10404  modqge0  10426  modqlt  10427  modqid  10443  m1modge3gt1  10465  modaddmodup  10481  addmodlteq  10492  ser3mono  10581  seqf1oglem1  10613  seqf1oglem2  10614  ser3ge0  10630  ser3le  10631  leexp1a  10688  sqgt0ap  10702  sqge0  10710  nnlesq  10737  expnbnd  10757  nn0opthlem2d  10815  facwordi  10834  filtinf  10885  hashunlem  10898  zfz1isolemiso  10933  cjmulge0  11056  resqrexlemover  11177  resqrexlemdec  11178  resqrexlemlo  11180  resqrexlemcalc3  11183  resqrexlemcvg  11186  resqrexlemoverl  11188  resqrexlemglsq  11189  resqrexlemga  11190  absge0  11227  amgm2  11285  maxle1  11378  bdtrilem  11406  xrmaxifle  11413  xrmaxiflemlub  11415  xrmaxiflemval  11417  xrmax1sup  11420  xrmaxltsup  11425  xrmaxadd  11428  xrbdtri  11443  reccn2ap  11480  climle  11501  climserle  11512  isumclim2  11589  isumclim3  11590  isumge0  11597  fsumlessfi  11627  expcnvap0  11669  expcnvre  11670  explecnv  11672  absltap  11676  cvgratnnlembern  11690  cvgratnnlemnexp  11691  cvgratnnlemmn  11692  cvgratnnlemabsle  11694  cvgratnnlemfm  11696  cvgratnnlemrate  11697  mertenslemi1  11702  mertenslem2  11703  clim2divap  11707  prodmodclem3  11742  efcvg  11833  ege2le3  11838  efaddlem  11841  eftlub  11857  effsumlt  11859  ef01bndlem  11923  sin02gt0  11931  eirrap  11945  iddvdsexp  11982  dvdsadd  12003  dvdsfac  12027  dvdsmod  12029  3dvds  12031  omoe  12063  divalglemnn  12085  divalglemnqt  12087  flodddiv4t2lthalf  12106  bitsfzo  12122  bitsmod  12123  bitscmp  12125  bitsinv1lem  12128  dvdslegcd  12141  dfgcd3  12187  dvdssqim  12201  dvdsmulgcd  12202  nn0seqcvgd  12219  dvdslcm  12247  lcmgcdlem  12255  mulgcddvds  12272  qredeq  12274  cncongr2  12282  sqnprm  12314  isprm6  12325  sqpweven  12353  znege1  12356  sqrt2irrap  12358  nonsq  12385  hashdvds  12399  prmdiv  12413  odzdvds  12424  pythagtriplem4  12447  pcpre1  12471  pcdvdsb  12499  pcz  12511  pcprmpw2  12512  pcaddlem  12518  pcadd  12519  pcadd2  12520  pcmpt  12522  pcmptdvds  12524  fldivp1  12527  pcfaclem  12528  pockthlem  12535  4sqlem6  12562  4sqlem8  12564  4sqexercise1  12577  4sqexercise2  12578  4sqlemsdc  12579  4sqlem11  12580  4sqlem12  12581  4sqlem14  12583  4sqlem16  12585  ennnfonelemkh  12639  nninfdclemp1  12677  eqgen  13367  dvdsrmul1  13668  unitmulclb  13680  subrguss  13802  znidom  14223  znunit  14225  psmetxrge0  14578  isxmet2d  14594  mettri  14619  xmettri3  14620  mettri3  14621  xblss2ps  14650  blss2ps  14652  blss2  14653  blssps  14673  blss  14674  xmetxp  14753  ivthdec  14890  ivthreinc  14891  hoverb  14894  hovergt0  14896  sin0pilem1  15027  sinq12gt0  15076  tangtx  15084  cosordlem  15095  cosq34lt1  15096  logdivlti  15127  logbgcd1irrap  15216  perfectlem1  15245  lgsdilem2  15287  gausslemma2dlem1f1o  15311  lgsquadlem1  15328  2lgsoddprmlem2  15357  2sqlem3  15368  2sqlem8  15374  cvgcmp2nlemabs  15686  trilpolemclim  15690  trilpolemeq1  15694  apdifflemf  15700  apdifflemr  15701  nconstwlpolemgt0  15718