Theorem breqtri 5125

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

Syntax hints:   = wceq 1542   class class class wbr 5100

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  breqtrri  5127  3brtr3i  5129  supsrlem  11036  0lt1  11673  le9lt10  12648  9lt10  12752  hashunlei  14362  sqrt2gt1lt2  15211  trireciplem  15799  cos1bnd  16126  cos2bnd  16127  cos01gt0  16130  sin4lt0  16134  rpnnen2lem3  16155  z4even  16313  gcdaddmlem  16465  dec2dvds  17005  abvtrivd  20782  sincos4thpi  26495  log2cnv  26927  log2ublem2  26930  log2ublem3  26931  log2le1  26933  birthday  26937  harmonicbnd3  26991  lgam1  27047  basellem7  27070  ppiublem1  27186  ppiub  27188  bposlem4  27271  bposlem5  27272  bposlem9  27276  lgsdir2lem2  27310  lgsdir2lem3  27311  1reno  28510  ex-fl  30540  siilem1  30945  normlem5  31208  normlem6  31209  norm-ii-i  31231  norm3adifii  31242  cmm2i  31701  mayetes3i  31823  nmopcoadji  32195  mdoc2i  32520  dmdoc2i  32522  dp2lt10  32982  dp2ltsuc  32984  dplti  33003  sqsscirc1  34092  ballotlem1c  34692  hgt750lem  34835  problem5  35891  circum  35896  bj-pinftyccb  37503  bj-minftyccb  37507  poimirlem25  37925  cntotbnd  38076  3lexlogpow5ineq1  42453  3lexlogpow5ineq2  42454  aks4d1p1p2  42469  aks4d1p1p7  42473  posbezout  42499  aks6d1c7lem1  42579  jm2.23  43382  tr3dom  43913  halffl  45687  wallispi  46457  stirlinglem1  46461  fouriersw  46618  sinnpoly  47280