Theorem breqtrrd 4033

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 4031	1 |- ( ph -> A R C )

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

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 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-br 4006

This theorem is referenced by:  frirrg  4352  unsnfidcex  6921  unsnfidcel  6922  addlocprlemeq  7534  ltexprlemopl  7602  recexprlemloc  7632  cauappcvgprlemopl  7647  cauappcvgprlemladdfu  7655  cauappcvgprlem1  7660  caucvgprlemopl  7670  caucvgprlemladdfu  7678  caucvgprprlemopl  7698  caucvgprprlemexbt  7707  mulgt0sr  7779  archsr  7783  caucvgsrlemoffgt1  7800  suplocsrlemb  7807  suplocsrlem  7809  mulap0r  8574  prodgt0  8811  div4p1lem1div2  9174  mul2lt0rgt0  9762  xnn0dcle  9804  xnn0letri  9805  xleadd1a  9875  xltadd1  9878  xlt2add  9882  xposdif  9884  xlesubadd  9885  xleaddadd  9889  uzsubsubfz  10049  fzctr  10135  subfzo0  10244  exbtwnzlemstep  10250  exbtwnzlemex  10252  rebtwn2zlemstep  10255  rebtwn2z  10257  qbtwnxr  10260  ceilqge  10312  modqge0  10334  modqlt  10335  modqid  10351  m1modge3gt1  10373  modaddmodup  10389  addmodlteq  10400  ser3mono  10480  ser3ge0  10519  ser3le  10520  leexp1a  10577  sqgt0ap  10591  sqge0  10599  nnlesq  10626  expnbnd  10646  nn0opthlem2d  10703  facwordi  10722  filtinf  10773  hashunlem  10786  zfz1isolemiso  10821  cjmulge0  10900  resqrexlemover  11021  resqrexlemdec  11022  resqrexlemlo  11024  resqrexlemcalc3  11027  resqrexlemcvg  11030  resqrexlemoverl  11032  resqrexlemglsq  11033  resqrexlemga  11034  absge0  11071  amgm2  11129  maxle1  11222  bdtrilem  11249  xrmaxifle  11256  xrmaxiflemlub  11258  xrmaxiflemval  11260  xrmax1sup  11263  xrmaxltsup  11268  xrmaxadd  11271  xrbdtri  11286  reccn2ap  11323  climle  11344  climserle  11355  isumclim2  11432  isumclim3  11433  isumge0  11440  fsumlessfi  11470  expcnvap0  11512  expcnvre  11513  explecnv  11515  absltap  11519  cvgratnnlembern  11533  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  cvgratnnlemabsle  11537  cvgratnnlemfm  11539  cvgratnnlemrate  11540  mertenslemi1  11545  mertenslem2  11546  clim2divap  11550  prodmodclem3  11585  efcvg  11676  ege2le3  11681  efaddlem  11684  eftlub  11700  effsumlt  11702  ef01bndlem  11766  sin02gt0  11773  eirrap  11787  iddvdsexp  11824  dvdsadd  11845  dvdsfac  11868  dvdsmod  11870  omoe  11903  divalglemnn  11925  divalglemnqt  11927  flodddiv4t2lthalf  11944  dvdslegcd  11967  dfgcd3  12013  dvdssqim  12027  dvdsmulgcd  12028  nn0seqcvgd  12043  dvdslcm  12071  lcmgcdlem  12079  mulgcddvds  12096  qredeq  12098  cncongr2  12106  sqnprm  12138  isprm6  12149  sqpweven  12177  znege1  12180  sqrt2irrap  12182  nonsq  12209  hashdvds  12223  prmdiv  12237  odzdvds  12247  pythagtriplem4  12270  pcpre1  12294  pcdvdsb  12321  pcz  12333  pcprmpw2  12334  pcaddlem  12340  pcadd  12341  pcmpt  12343  pcmptdvds  12345  fldivp1  12348  pcfaclem  12349  pockthlem  12356  4sqlem6  12383  4sqlem8  12385  ennnfonelemkh  12415  nninfdclemp1  12453  eqgen  13091  dvdsrmul1  13276  unitmulclb  13288  subrguss  13362  psmetxrge0  13871  isxmet2d  13887  mettri  13912  xmettri3  13913  mettri3  13914  xblss2ps  13943  blss2ps  13945  blss2  13946  blssps  13966  blss  13967  xmetxp  14046  ivthdec  14161  sin0pilem1  14241  sinq12gt0  14290  tangtx  14298  cosordlem  14309  cosq34lt1  14310  logdivlti  14341  logbgcd1irrap  14427  lgsdilem2  14476  2lgsoddprmlem2  14493  2sqlem3  14503  2sqlem8  14509  cvgcmp2nlemabs  14819  trilpolemclim  14823  trilpolemeq1  14827  apdifflemf  14833  apdifflemr  14834  nconstwlpolemgt0  14851