Theorem breqtri 5127

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

Syntax hints:   = wceq 1540   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  breqtrri  5129  3brtr3i  5131  supsrlem  11040  0lt1  11676  le9lt10  12652  9lt10  12756  hashunlei  14366  sqrt2gt1lt2  15216  trireciplem  15804  cos1bnd  16131  cos2bnd  16132  cos01gt0  16135  sin4lt0  16139  rpnnen2lem3  16160  z4even  16318  gcdaddmlem  16470  dec2dvds  17010  abvtrivd  20752  sincos4thpi  26455  log2cnv  26887  log2ublem2  26890  log2ublem3  26891  log2le1  26893  birthday  26897  harmonicbnd3  26951  lgam1  27007  basellem7  27030  ppiublem1  27146  ppiub  27148  bposlem4  27231  bposlem5  27232  bposlem9  27236  lgsdir2lem2  27270  lgsdir2lem3  27271  0reno  28401  ex-fl  30426  siilem1  30830  normlem5  31093  normlem6  31094  norm-ii-i  31116  norm3adifii  31127  cmm2i  31586  mayetes3i  31708  nmopcoadji  32080  mdoc2i  32405  dmdoc2i  32407  dp2lt10  32854  dp2ltsuc  32856  dplti  32875  sqsscirc1  33891  ballotlem1c  34492  hgt750lem  34635  problem5  35649  circum  35654  bj-pinftyccb  37202  bj-minftyccb  37206  poimirlem25  37632  cntotbnd  37783  3lexlogpow5ineq1  42035  3lexlogpow5ineq2  42036  aks4d1p1p2  42051  aks4d1p1p7  42055  posbezout  42081  aks6d1c7lem1  42161  jm2.23  42978  tr3dom  43510  halffl  45287  wallispi  46061  stirlinglem1  46065  fouriersw  46222  sinnpoly  46885