Theorem breqtrrd 3893

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

Syntax hints:   -> wi 4   = wceq 1296   class class class wbr 3867

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-br 3868

This theorem is referenced by:  frirrg  4201  unsnfidcex  6710  unsnfidcel  6711  addlocprlemeq  7189  ltexprlemopl  7257  recexprlemloc  7287  cauappcvgprlemopl  7302  cauappcvgprlemladdfu  7310  cauappcvgprlem1  7315  caucvgprlemopl  7325  caucvgprlemladdfu  7333  caucvgprprlemopl  7353  caucvgprprlemexbt  7362  mulgt0sr  7420  archsr  7424  caucvgsrlemoffgt1  7441  mulap0r  8189  prodgt0  8410  div4p1lem1div2  8767  xleadd1a  9439  xltadd1  9442  xlt2add  9446  xposdif  9448  xlesubadd  9449  xleaddadd  9453  uzsubsubfz  9610  fzctr  9693  subfzo0  9802  exbtwnzlemstep  9808  exbtwnzlemex  9810  rebtwn2zlemstep  9813  rebtwn2z  9815  qbtwnxr  9818  ceilqge  9866  modqge0  9888  modqlt  9889  modqid  9905  m1modge3gt1  9927  modaddmodup  9943  addmodlteq  9954  ser3mono  10028  ser3ge0  10067  ser3le  10068  leexp1a  10125  sqgt0ap  10138  sqge0  10146  nnlesq  10173  expnbnd  10192  nn0opthlem2d  10244  facwordi  10263  filtinf  10315  hashunlem  10327  zfz1isolemiso  10359  cjmulge0  10438  resqrexlemover  10558  resqrexlemdec  10559  resqrexlemlo  10561  resqrexlemcalc3  10564  resqrexlemcvg  10567  resqrexlemoverl  10569  resqrexlemglsq  10570  resqrexlemga  10571  absge0  10608  amgm2  10666  maxle1  10759  bdtrilem  10785  xrmaxifle  10789  xrmaxiflemlub  10791  xrmaxiflemval  10793  xrmax1sup  10796  xrmaxltsup  10801  xrmaxadd  10804  xrbdtri  10819  reccn2ap  10856  climle  10877  climserle  10888  isumclim2  10965  isumclim3  10966  isumge0  10973  fsumlessfi  11003  expcnvap0  11045  expcnvre  11046  explecnv  11048  absltap  11052  cvgratnnlembern  11066  cvgratnnlemnexp  11067  cvgratnnlemmn  11068  cvgratnnlemabsle  11070  cvgratnnlemfm  11072  cvgratnnlemrate  11073  mertenslemi1  11078  mertenslem2  11079  efcvg  11105  ege2le3  11110  efaddlem  11113  eftlub  11129  effsumlt  11131  ef01bndlem  11196  sin02gt0  11203  eirrap  11214  iddvdsexp  11247  dvdsadd  11266  dvdsfac  11288  dvdsmod  11290  omoe  11323  divalglemnn  11345  divalglemnqt  11347  flodddiv4t2lthalf  11364  dvdslegcd  11383  dfgcd3  11426  dvdssqim  11440  dvdsmulgcd  11441  nn0seqcvgd  11450  dvdslcm  11478  lcmgcdlem  11486  mulgcddvds  11503  qredeq  11505  cncongr2  11513  sqnprm  11544  isprm6  11553  sqpweven  11580  znege1  11583  sqrt2irrap  11585  nonsq  11612  hashdvds  11624  psmetxrge0  12118  isxmet2d  12134  mettri  12159  xmettri3  12160  mettri3  12161  xblss2ps  12190  blss2ps  12192  blss2  12193  blssps  12213  blss  12214