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 229	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1534   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 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143

This theorem is referenced by:  breqtrri  5169  3brtr3i  5171  supsrlem  11128  0lt1  11760  le9lt10  12728  9lt10  12832  hashunlei  14410  sqrt2gt1lt2  15247  trireciplem  15834  cos1bnd  16157  cos2bnd  16158  cos01gt0  16161  sin4lt0  16165  rpnnen2lem3  16186  z4even  16342  gcdaddmlem  16492  dec2dvds  17025  abvtrivd  20713  sincos4thpi  26441  log2cnv  26869  log2ublem2  26872  log2ublem3  26873  log2le1  26875  birthday  26879  harmonicbnd3  26933  lgam1  26989  basellem7  27012  ppiublem1  27128  ppiub  27130  bposlem4  27213  bposlem5  27214  bposlem9  27218  lgsdir2lem2  27252  lgsdir2lem3  27253  0reno  28218  ex-fl  30250  siilem1  30654  normlem5  30917  normlem6  30918  norm-ii-i  30940  norm3adifii  30951  cmm2i  31410  mayetes3i  31532  nmopcoadji  31904  mdoc2i  32229  dmdoc2i  32231  dp2lt10  32601  dp2ltsuc  32603  dplti  32622  sqsscirc1  33503  ballotlem1c  34121  hgt750lem  34277  problem5  35267  circum  35272  bj-pinftyccb  36694  bj-minftyccb  36698  poimirlem25  37112  cntotbnd  37263  3lexlogpow5ineq1  41519  3lexlogpow5ineq2  41520  aks4d1p1p2  41535  aks4d1p1p7  41539  posbezout  41565  aks6d1c7lem1  41646  jm2.23  42411  tr3dom  42952  halffl  44672  wallispi  45452  stirlinglem1  45456  fouriersw  45613