Theorem breqtri 5135

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

Syntax hints:   = wceq 1541   class class class wbr 5110

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111

This theorem is referenced by:  breqtrri  5137  3brtr3i  5139  supsrlem  11056  0lt1  11686  le9lt10  12654  9lt10  12758  hashunlei  14335  sqrt2gt1lt2  15171  trireciplem  15758  cos1bnd  16080  cos2bnd  16081  cos01gt0  16084  sin4lt0  16088  rpnnen2lem3  16109  z4even  16265  gcdaddmlem  16415  dec2dvds  16946  abvtrivd  20355  sincos4thpi  25907  log2cnv  26331  log2ublem2  26334  log2ublem3  26335  log2le1  26337  birthday  26341  harmonicbnd3  26394  lgam1  26450  basellem7  26473  ppiublem1  26587  ppiub  26589  bposlem4  26672  bposlem5  26673  bposlem9  26677  lgsdir2lem2  26711  lgsdir2lem3  26712  ex-fl  29454  siilem1  29856  normlem5  30119  normlem6  30120  norm-ii-i  30142  norm3adifii  30153  cmm2i  30612  mayetes3i  30734  nmopcoadji  31106  mdoc2i  31431  dmdoc2i  31433  dp2lt10  31810  dp2ltsuc  31812  dplti  31831  sqsscirc1  32578  ballotlem1c  33196  hgt750lem  33353  problem5  34344  circum  34349  bj-pinftyccb  35765  bj-minftyccb  35769  poimirlem25  36176  cntotbnd  36328  3lexlogpow5ineq1  40584  3lexlogpow5ineq2  40585  aks4d1p1p2  40600  aks4d1p1p7  40604  jm2.23  41378  tr3dom  41922  halffl  43651  wallispi  44431  stirlinglem1  44435  fouriersw  44592