Theorem breqtri 5173

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 5156	. 2 ⊢ (𝐴𝑅𝐵 ↔ 𝐴𝑅𝐶)
4	1, 3	mpbi 230	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1537   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149

This theorem is referenced by:  breqtrri  5175  3brtr3i  5177  supsrlem  11149  0lt1  11783  le9lt10  12758  9lt10  12862  hashunlei  14461  sqrt2gt1lt2  15310  trireciplem  15895  cos1bnd  16220  cos2bnd  16221  cos01gt0  16224  sin4lt0  16228  rpnnen2lem3  16249  z4even  16406  gcdaddmlem  16558  dec2dvds  17097  abvtrivd  20850  sincos4thpi  26570  log2cnv  27002  log2ublem2  27005  log2ublem3  27006  log2le1  27008  birthday  27012  harmonicbnd3  27066  lgam1  27122  basellem7  27145  ppiublem1  27261  ppiub  27263  bposlem4  27346  bposlem5  27347  bposlem9  27351  lgsdir2lem2  27385  lgsdir2lem3  27386  0reno  28444  ex-fl  30476  siilem1  30880  normlem5  31143  normlem6  31144  norm-ii-i  31166  norm3adifii  31177  cmm2i  31636  mayetes3i  31758  nmopcoadji  32130  mdoc2i  32455  dmdoc2i  32457  dp2lt10  32851  dp2ltsuc  32853  dplti  32872  sqsscirc1  33869  ballotlem1c  34489  hgt750lem  34645  problem5  35654  circum  35659  bj-pinftyccb  37204  bj-minftyccb  37208  poimirlem25  37632  cntotbnd  37783  3lexlogpow5ineq1  42036  3lexlogpow5ineq2  42037  aks4d1p1p2  42052  aks4d1p1p7  42056  posbezout  42082  aks6d1c7lem1  42162  jm2.23  42985  tr3dom  43518  halffl  45247  wallispi  46026  stirlinglem1  46030  fouriersw  46187