Theorem breqtri 5121

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
breqtr.1	⊢ 𝐴𝑅𝐵
breqtr.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
breqtri	⊢ 𝐴𝑅𝐶

Proof of Theorem breqtri

Step	Hyp	Ref	Expression
1		breqtr.1	. 2 ⊢ 𝐴𝑅𝐵
2		breqtr.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	breq2i 5104	. 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶)
4	1, 3	mpbi 230	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1541   class class class wbr 5096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097

This theorem is referenced by:  breqtrri  5123  3brtr3i  5125  supsrlem  11020  0lt1  11657  le9lt10  12632  9lt10  12736  hashunlei  14346  sqrt2gt1lt2  15195  trireciplem  15783  cos1bnd  16110  cos2bnd  16111  cos01gt0  16114  sin4lt0  16118  rpnnen2lem3  16139  z4even  16297  gcdaddmlem  16449  dec2dvds  16989  abvtrivd  20763  sincos4thpi  26476  log2cnv  26908  log2ublem2  26911  log2ublem3  26912  log2le1  26914  birthday  26918  harmonicbnd3  26972  lgam1  27028  basellem7  27051  ppiublem1  27167  ppiub  27169  bposlem4  27252  bposlem5  27253  bposlem9  27257  lgsdir2lem2  27291  lgsdir2lem3  27292  1reno  28442  ex-fl  30471  siilem1  30875  normlem5  31138  normlem6  31139  norm-ii-i  31161  norm3adifii  31172  cmm2i  31631  mayetes3i  31753  nmopcoadji  32125  mdoc2i  32450  dmdoc2i  32452  dp2lt10  32914  dp2ltsuc  32916  dplti  32935  sqsscirc1  34014  ballotlem1c  34614  hgt750lem  34757  problem5  35812  circum  35817  bj-pinftyccb  37365  bj-minftyccb  37369  poimirlem25  37785  cntotbnd  37936  3lexlogpow5ineq1  42247  3lexlogpow5ineq2  42248  aks4d1p1p2  42263  aks4d1p1p7  42267  posbezout  42293  aks6d1c7lem1  42373  jm2.23  43180  tr3dom  43711  halffl  45486  wallispi  46256  stirlinglem1  46260  fouriersw  46417  sinnpoly  47079