Theorem breqtrrd 3964

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

Syntax hints:   -> wi 4   = wceq 1332   class class class wbr 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-br 3938

This theorem is referenced by:  frirrg  4280  unsnfidcex  6816  unsnfidcel  6817  addlocprlemeq  7365  ltexprlemopl  7433  recexprlemloc  7463  cauappcvgprlemopl  7478  cauappcvgprlemladdfu  7486  cauappcvgprlem1  7491  caucvgprlemopl  7501  caucvgprlemladdfu  7509  caucvgprprlemopl  7529  caucvgprprlemexbt  7538  mulgt0sr  7610  archsr  7614  caucvgsrlemoffgt1  7631  suplocsrlemb  7638  suplocsrlem  7640  mulap0r  8401  prodgt0  8634  div4p1lem1div2  8997  mul2lt0rgt0  9577  xleadd1a  9686  xltadd1  9689  xlt2add  9693  xposdif  9695  xlesubadd  9696  xleaddadd  9700  uzsubsubfz  9858  fzctr  9941  subfzo0  10050  exbtwnzlemstep  10056  exbtwnzlemex  10058  rebtwn2zlemstep  10061  rebtwn2z  10063  qbtwnxr  10066  ceilqge  10114  modqge0  10136  modqlt  10137  modqid  10153  m1modge3gt1  10175  modaddmodup  10191  addmodlteq  10202  ser3mono  10282  ser3ge0  10321  ser3le  10322  leexp1a  10379  sqgt0ap  10392  sqge0  10400  nnlesq  10427  expnbnd  10446  nn0opthlem2d  10499  facwordi  10518  filtinf  10570  hashunlem  10582  zfz1isolemiso  10614  cjmulge0  10693  resqrexlemover  10814  resqrexlemdec  10815  resqrexlemlo  10817  resqrexlemcalc3  10820  resqrexlemcvg  10823  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemga  10827  absge0  10864  amgm2  10922  maxle1  11015  bdtrilem  11042  xrmaxifle  11047  xrmaxiflemlub  11049  xrmaxiflemval  11051  xrmax1sup  11054  xrmaxltsup  11059  xrmaxadd  11062  xrbdtri  11077  reccn2ap  11114  climle  11135  climserle  11146  isumclim2  11223  isumclim3  11224  isumge0  11231  fsumlessfi  11261  expcnvap0  11303  expcnvre  11304  explecnv  11306  absltap  11310  cvgratnnlembern  11324  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratnnlemabsle  11328  cvgratnnlemfm  11330  cvgratnnlemrate  11331  mertenslemi1  11336  mertenslem2  11337  clim2divap  11341  prodmodclem3  11376  efcvg  11409  ege2le3  11414  efaddlem  11417  eftlub  11433  effsumlt  11435  ef01bndlem  11499  sin02gt0  11506  eirrap  11520  iddvdsexp  11553  dvdsadd  11572  dvdsfac  11594  dvdsmod  11596  omoe  11629  divalglemnn  11651  divalglemnqt  11653  flodddiv4t2lthalf  11670  dvdslegcd  11689  dfgcd3  11734  dvdssqim  11748  dvdsmulgcd  11749  nn0seqcvgd  11758  dvdslcm  11786  lcmgcdlem  11794  mulgcddvds  11811  qredeq  11813  cncongr2  11821  sqnprm  11852  isprm6  11861  sqpweven  11889  znege1  11892  sqrt2irrap  11894  nonsq  11921  hashdvds  11933  ennnfonelemkh  11961  psmetxrge0  12540  isxmet2d  12556  mettri  12581  xmettri3  12582  mettri3  12583  xblss2ps  12612  blss2ps  12614  blss2  12615  blssps  12635  blss  12636  xmetxp  12715  ivthdec  12830  sin0pilem1  12910  sinq12gt0  12959  tangtx  12967  cosordlem  12978  cosq34lt1  12979  logdivlti  13010  logbgcd1irrap  13095  cvgcmp2nlemabs  13402  trilpolemclim  13404  trilpolemeq1  13408  apdifflemf  13414  apdifflemr  13415