Theorem breqtrrd 4031

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

Syntax hints:   -> wi 4   = wceq 1353   class class class wbr 4003

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004

This theorem is referenced by:  frirrg  4350  unsnfidcex  6918  unsnfidcel  6919  addlocprlemeq  7531  ltexprlemopl  7599  recexprlemloc  7629  cauappcvgprlemopl  7644  cauappcvgprlemladdfu  7652  cauappcvgprlem1  7657  caucvgprlemopl  7667  caucvgprlemladdfu  7675  caucvgprprlemopl  7695  caucvgprprlemexbt  7704  mulgt0sr  7776  archsr  7780  caucvgsrlemoffgt1  7797  suplocsrlemb  7804  suplocsrlem  7806  mulap0r  8571  prodgt0  8808  div4p1lem1div2  9171  mul2lt0rgt0  9759  xnn0dcle  9801  xnn0letri  9802  xleadd1a  9872  xltadd1  9875  xlt2add  9879  xposdif  9881  xlesubadd  9882  xleaddadd  9886  uzsubsubfz  10046  fzctr  10132  subfzo0  10241  exbtwnzlemstep  10247  exbtwnzlemex  10249  rebtwn2zlemstep  10252  rebtwn2z  10254  qbtwnxr  10257  ceilqge  10309  modqge0  10331  modqlt  10332  modqid  10348  m1modge3gt1  10370  modaddmodup  10386  addmodlteq  10397  ser3mono  10477  ser3ge0  10516  ser3le  10517  leexp1a  10574  sqgt0ap  10588  sqge0  10596  nnlesq  10623  expnbnd  10643  nn0opthlem2d  10700  facwordi  10719  filtinf  10770  hashunlem  10783  zfz1isolemiso  10818  cjmulge0  10897  resqrexlemover  11018  resqrexlemdec  11019  resqrexlemlo  11021  resqrexlemcalc3  11024  resqrexlemcvg  11027  resqrexlemoverl  11029  resqrexlemglsq  11030  resqrexlemga  11031  absge0  11068  amgm2  11126  maxle1  11219  bdtrilem  11246  xrmaxifle  11253  xrmaxiflemlub  11255  xrmaxiflemval  11257  xrmax1sup  11260  xrmaxltsup  11265  xrmaxadd  11268  xrbdtri  11283  reccn2ap  11320  climle  11341  climserle  11352  isumclim2  11429  isumclim3  11430  isumge0  11437  fsumlessfi  11467  expcnvap0  11509  expcnvre  11510  explecnv  11512  absltap  11516  cvgratnnlembern  11530  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratnnlemabsle  11534  cvgratnnlemfm  11536  cvgratnnlemrate  11537  mertenslemi1  11542  mertenslem2  11543  clim2divap  11547  prodmodclem3  11582  efcvg  11673  ege2le3  11678  efaddlem  11681  eftlub  11697  effsumlt  11699  ef01bndlem  11763  sin02gt0  11770  eirrap  11784  iddvdsexp  11821  dvdsadd  11842  dvdsfac  11865  dvdsmod  11867  omoe  11900  divalglemnn  11922  divalglemnqt  11924  flodddiv4t2lthalf  11941  dvdslegcd  11964  dfgcd3  12010  dvdssqim  12024  dvdsmulgcd  12025  nn0seqcvgd  12040  dvdslcm  12068  lcmgcdlem  12076  mulgcddvds  12093  qredeq  12095  cncongr2  12103  sqnprm  12135  isprm6  12146  sqpweven  12174  znege1  12177  sqrt2irrap  12179  nonsq  12206  hashdvds  12220  prmdiv  12234  odzdvds  12244  pythagtriplem4  12267  pcpre1  12291  pcdvdsb  12318  pcz  12330  pcprmpw2  12331  pcaddlem  12337  pcadd  12338  pcmpt  12340  pcmptdvds  12342  fldivp1  12345  pcfaclem  12346  pockthlem  12353  4sqlem6  12380  4sqlem8  12382  ennnfonelemkh  12412  nninfdclemp1  12450  eqgen  13084  dvdsrmul1  13269  unitmulclb  13281  subrguss  13355  psmetxrge0  13802  isxmet2d  13818  mettri  13843  xmettri3  13844  mettri3  13845  xblss2ps  13874  blss2ps  13876  blss2  13877  blssps  13897  blss  13898  xmetxp  13977  ivthdec  14092  sin0pilem1  14172  sinq12gt0  14221  tangtx  14229  cosordlem  14240  cosq34lt1  14241  logdivlti  14272  logbgcd1irrap  14358  lgsdilem2  14407  2lgsoddprmlem2  14424  2sqlem3  14434  2sqlem8  14440  cvgcmp2nlemabs  14750  trilpolemclim  14754  trilpolemeq1  14758  apdifflemf  14764  apdifflemr  14765  nconstwlpolemgt0  14781