Theorem breqtri 4710

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

Syntax hints:   = wceq 1523   class class class wbr 4685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686

This theorem is referenced by:  breqtrri  4712  3brtr3i  4714  supsrlem  9970  0lt1  10588  le9lt10  11567  9lt10  11711  hashunlei  13250  sqrt2gt1lt2  14059  trireciplem  14638  cos1bnd  14961  cos2bnd  14962  cos01gt0  14965  sin4lt0  14969  rpnnen2lem3  14989  z4even  15155  gcdaddmlem  15292  dec2dvds  15814  abvtrivd  18888  sincos4thpi  24310  log2cnv  24716  log2ublem2  24719  log2ublem3  24720  log2le1  24722  birthday  24726  harmonicbnd3  24779  lgam1  24835  basellem7  24858  ppiublem1  24972  ppiublem2  24973  ppiub  24974  bposlem4  25057  bposlem5  25058  bposlem9  25062  lgsdir2lem2  25096  lgsdir2lem3  25097  ex-fl  27434  siilem1  27834  normlem5  28099  normlem6  28100  norm-ii-i  28122  norm3adifii  28133  cmm2i  28594  mayetes3i  28716  nmopcoadji  29088  mdoc2i  29413  dmdoc2i  29415  dp2lt10  29719  dp2ltsuc  29721  dplti  29741  sqsscirc1  30082  ballotlem1c  30697  hgt750lem  30857  problem5  31689  circum  31694  bj-pinftyccb  33238  bj-minftyccb  33242  poimirlem25  33564  cntotbnd  33725  jm2.23  37880  halffl  39824  wallispi  40605  stirlinglem1  40609  fouriersw  40766