Theorem breqtri 5095

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

Syntax hints:   = wceq 1543   class class class wbr 5070

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 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  breqtrri  5097  3brtr3i  5099  supsrlem  10773  0lt1  11402  le9lt10  12368  9lt10  12472  hashunlei  14043  sqrt2gt1lt2  14889  trireciplem  15477  cos1bnd  15799  cos2bnd  15800  cos01gt0  15803  sin4lt0  15807  rpnnen2lem3  15828  z4even  15984  gcdaddmlem  16134  dec2dvds  16667  abvtrivd  19990  sincos4thpi  25550  log2cnv  25974  log2ublem2  25977  log2ublem3  25978  log2le1  25980  birthday  25984  harmonicbnd3  26037  lgam1  26093  basellem7  26116  ppiublem1  26230  ppiub  26232  bposlem4  26315  bposlem5  26316  bposlem9  26320  lgsdir2lem2  26354  lgsdir2lem3  26355  ex-fl  28687  siilem1  29089  normlem5  29352  normlem6  29353  norm-ii-i  29375  norm3adifii  29386  cmm2i  29845  mayetes3i  29967  nmopcoadji  30339  mdoc2i  30664  dmdoc2i  30666  dp2lt10  31035  dp2ltsuc  31037  dplti  31056  sqsscirc1  31735  ballotlem1c  32349  hgt750lem  32506  problem5  33502  circum  33507  bj-pinftyccb  35295  bj-minftyccb  35299  poimirlem25  35708  cntotbnd  35860  3lexlogpow5ineq1  39969  3lexlogpow5ineq2  39970  aks4d1p1p2  39984  aks4d1p1p7  39988  jm2.23  40706  tr3dom  41005  halffl  42698  wallispi  43474  stirlinglem1  43478  fouriersw  43635