Theorem breqtri 5100

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

Syntax hints:   = wceq 1548   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  breqtrri  5102  3brtr3i  5104  supsrlem  11029  0lt1  11667  le9lt10  12666  9lt10  12770  hashunlei  14382  sqrt2gt1lt2  15231  trireciplem  15822  cos1bnd  16149  cos2bnd  16150  cos01gt0  16153  sin4lt0  16157  rpnnen2lem3  16178  z4even  16336  gcdaddmlem  16488  dec2dvds  17029  abvtrivd  20808  sincos4thpi  26499  log2cnv  26930  log2ublem2  26933  log2ublem3  26934  log2le1  26936  birthday  26940  harmonicbnd3  26993  lgam1  27049  basellem7  27072  ppiublem1  27187  ppiub  27189  bposlem4  27272  bposlem5  27273  bposlem9  27277  lgsdir2lem2  27311  lgsdir2lem3  27312  1reno  28511  ex-fl  30539  siilem1  30944  normlem5  31207  normlem6  31208  norm-ii-i  31230  norm3adifii  31241  cmm2i  31700  mayetes3i  31822  nmopcoadji  32194  mdoc2i  32519  dmdoc2i  32521  dp2lt10  32966  dp2ltsuc  32968  dplti  32987  sqsscirc1  34104  ballotlem1c  34704  hgt750lem  34847  problem5  35912  circum  35917  bj-pinftyccb  37596  bj-minftyccb  37600  poimirlem25  38027  cntotbnd  38178  3lexlogpow5ineq1  42554  3lexlogpow5ineq2  42555  aks4d1p1p2  42570  aks4d1p1p7  42574  posbezout  42600  aks6d1c7lem1  42680  jm2.23  43456  tr3dom  43987  halffl  45758  wallispi  46527  stirlinglem1  46531  fouriersw  46688  sinnpoly  47368