Theorem breqtrrd 4139

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

Syntax hints:   -> wi 4   = wceq 1398   class class class wbr 4111

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112

This theorem is referenced by:  frirrg  4473  fidcen  7158  unsnfidcex  7182  unsnfidcel  7183  addlocprlemeq  7850  ltexprlemopl  7918  recexprlemloc  7948  cauappcvgprlemopl  7963  cauappcvgprlemladdfu  7971  cauappcvgprlem1  7976  caucvgprlemopl  7986  caucvgprlemladdfu  7994  caucvgprprlemopl  8014  caucvgprprlemexbt  8023  mulgt0sr  8095  archsr  8099  caucvgsrlemoffgt1  8116  suplocsrlemb  8123  suplocsrlem  8125  mulap0r  8891  prodgt0  9128  div4p1lem1div2  9494  mul2lt0rgt0  10096  xnn0dcle  10138  xnn0letri  10139  xleadd1a  10209  xltadd1  10212  xlt2add  10216  xposdif  10218  xlesubadd  10219  xleaddadd  10223  uzsubsubfz  10384  fzctr  10471  subfzo0  10592  exbtwnzlemstep  10611  exbtwnzlemex  10613  rebtwn2zlemstep  10616  rebtwn2z  10618  qbtwnxr  10621  xqltnle  10631  fldiv4lem1div2uz2  10670  ceilqge  10676  modqge0  10698  modqlt  10699  modqid  10715  m1modge3gt1  10737  modaddmodup  10753  addmodlteq  10764  ser3mono  10853  seqf1oglem1  10885  seqf1oglem2  10886  ser3ge0  10902  ser3le  10903  leexp1a  10960  sqgt0ap  10974  sqge0  10982  nnlesq  11009  expnbnd  11029  nn0opthlem2d  11087  facwordi  11106  bcm1n  11135  filtinf  11158  hashunlem  11172  zfz1isolemiso  11215  cats1fvd  11462  cjmulge0  11578  resqrexlemover  11699  resqrexlemdec  11700  resqrexlemlo  11702  resqrexlemcalc3  11705  resqrexlemcvg  11708  resqrexlemoverl  11710  resqrexlemglsq  11711  resqrexlemga  11712  absge0  11749  amgm2  11807  maxle1  11900  bdtrilem  11928  xrmaxifle  11935  xrmaxiflemlub  11937  xrmaxiflemval  11939  xrmax1sup  11942  xrmaxltsup  11947  xrmaxadd  11950  xrbdtri  11965  reccn2ap  12002  climle  12023  climserle  12034  isumclim2  12112  isumclim3  12113  isumge0  12120  fsumlessfi  12150  expcnvap0  12192  expcnvre  12193  explecnv  12195  absltap  12199  cvgratnnlembern  12213  cvgratnnlemnexp  12214  cvgratnnlemmn  12215  cvgratnnlemabsle  12217  cvgratnnlemfm  12219  cvgratnnlemrate  12220  mertenslemi1  12225  mertenslem2  12226  clim2divap  12230  prodmodclem3  12265  efcvg  12356  ege2le3  12361  efaddlem  12364  eftlub  12380  effsumlt  12382  ef01bndlem  12446  sin02gt0  12454  eirrap  12468  iddvdsexp  12505  dvdsadd  12526  dvdsfac  12550  dvdsmod  12552  3dvds  12554  omoe  12586  divalglemnn  12608  divalglemnqt  12610  flodddiv4t2lthalf  12629  bitsfzo  12645  bitsmod  12646  bitscmp  12648  bitsinv1lem  12651  dvdslegcd  12664  dfgcd3  12710  dvdssqim  12724  dvdsmulgcd  12725  nn0seqcvgd  12742  dvdslcm  12770  lcmgcdlem  12778  mulgcddvds  12795  qredeq  12797  cncongr2  12805  sqnprm  12837  isprm6  12848  sqpweven  12876  znege1  12879  sqrt2irrap  12881  nonsq  12908  hashdvds  12922  prmdiv  12936  odzdvds  12947  pythagtriplem4  12970  pcpre1  12994  pcdvdsb  13022  pcz  13034  pcprmpw2  13035  pcaddlem  13041  pcadd  13042  pcadd2  13043  pcmpt  13045  pcmptdvds  13047  fldivp1  13050  pcfaclem  13051  pockthlem  13058  4sqlem6  13085  4sqlem8  13087  4sqexercise1  13100  4sqexercise2  13101  4sqlemsdc  13102  4sqlem11  13103  4sqlem12  13104  4sqlem14  13106  4sqlem16  13108  ennnfonelemkh  13180  nninfdclemp1  13218  eqgen  13961  dvdsrmul1  14264  unitmulclb  14276  subrguss  14398  znidom  14822  znunit  14824  mplsubgfilemcl  14871  psmetxrge0  15214  isxmet2d  15230  mettri  15255  xmettri3  15256  mettri3  15257  xblss2ps  15286  blss2ps  15288  blss2  15289  blssps  15309  blss  15310  xmetxp  15389  ivthdec  15526  ivthreinc  15527  hoverb  15530  hovergt0  15532  sin0pilem1  15663  sinq12gt0  15712  tangtx  15720  cosordlem  15731  cosq34lt1  15732  logdivlti  15763  logbgcd1irrap  15852  perfectlem1  15884  lgsdilem2  15926  gausslemma2dlem1f1o  15950  lgsquadlem1  15967  2lgsoddprmlem2  15996  2sqlem3  16007  2sqlem8  16013  usgrsizedgen  16225  cvgcmp2nlemabs  16833  trilpolemclim  16837  trilpolemeq1  16841  apdifflemf  16847  apdifflemr  16848  nconstwlpolemgt0  16867