Theorem breqtri 5167

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

Syntax hints:   = wceq 1539   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143

This theorem is referenced by:  breqtrri  5169  3brtr3i  5171  supsrlem  11152  0lt1  11786  le9lt10  12762  9lt10  12866  hashunlei  14465  sqrt2gt1lt2  15314  trireciplem  15899  cos1bnd  16224  cos2bnd  16225  cos01gt0  16228  sin4lt0  16232  rpnnen2lem3  16253  z4even  16410  gcdaddmlem  16562  dec2dvds  17102  abvtrivd  20834  sincos4thpi  26556  log2cnv  26988  log2ublem2  26991  log2ublem3  26992  log2le1  26994  birthday  26998  harmonicbnd3  27052  lgam1  27108  basellem7  27131  ppiublem1  27247  ppiub  27249  bposlem4  27332  bposlem5  27333  bposlem9  27337  lgsdir2lem2  27371  lgsdir2lem3  27372  0reno  28430  ex-fl  30467  siilem1  30871  normlem5  31134  normlem6  31135  norm-ii-i  31157  norm3adifii  31168  cmm2i  31627  mayetes3i  31749  nmopcoadji  32121  mdoc2i  32446  dmdoc2i  32448  dp2lt10  32867  dp2ltsuc  32869  dplti  32888  sqsscirc1  33908  ballotlem1c  34511  hgt750lem  34667  problem5  35675  circum  35680  bj-pinftyccb  37223  bj-minftyccb  37227  poimirlem25  37653  cntotbnd  37804  3lexlogpow5ineq1  42056  3lexlogpow5ineq2  42057  aks4d1p1p2  42072  aks4d1p1p7  42076  posbezout  42102  aks6d1c7lem1  42182  jm2.23  43013  tr3dom  43546  halffl  45313  wallispi  46090  stirlinglem1  46094  fouriersw  46251