Theorem breqtri 5111

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

Syntax hints:   = wceq 1542   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  breqtrri  5113  3brtr3i  5115  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  20804  sincos4thpi  26494  log2cnv  26925  log2ublem2  26928  log2ublem3  26929  log2le1  26931  birthday  26935  harmonicbnd3  26989  lgam1  27045  basellem7  27068  ppiublem1  27183  ppiub  27185  bposlem4  27268  bposlem5  27269  bposlem9  27273  lgsdir2lem2  27307  lgsdir2lem3  27308  1reno  28507  ex-fl  30536  siilem1  30941  normlem5  31204  normlem6  31205  norm-ii-i  31227  norm3adifii  31238  cmm2i  31697  mayetes3i  31819  nmopcoadji  32191  mdoc2i  32516  dmdoc2i  32518  dp2lt10  32962  dp2ltsuc  32964  dplti  32983  sqsscirc1  34072  ballotlem1c  34672  hgt750lem  34815  problem5  35871  circum  35876  bj-pinftyccb  37555  bj-minftyccb  37559  poimirlem25  37984  cntotbnd  38135  3lexlogpow5ineq1  42511  3lexlogpow5ineq2  42512  aks4d1p1p2  42527  aks4d1p1p7  42531  posbezout  42557  aks6d1c7lem1  42637  jm2.23  43446  tr3dom  43977  halffl  45751  wallispi  46520  stirlinglem1  46524  fouriersw  46681  sinnpoly  47355