Theorem breqtri 5117

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

Syntax hints:   = wceq 1540   class class class wbr 5092

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  breqtrri  5119  3brtr3i  5121  supsrlem  11005  0lt1  11642  le9lt10  12618  9lt10  12722  hashunlei  14332  sqrt2gt1lt2  15181  trireciplem  15769  cos1bnd  16096  cos2bnd  16097  cos01gt0  16100  sin4lt0  16104  rpnnen2lem3  16125  z4even  16283  gcdaddmlem  16435  dec2dvds  16975  abvtrivd  20717  sincos4thpi  26420  log2cnv  26852  log2ublem2  26855  log2ublem3  26856  log2le1  26858  birthday  26862  harmonicbnd3  26916  lgam1  26972  basellem7  26995  ppiublem1  27111  ppiub  27113  bposlem4  27196  bposlem5  27197  bposlem9  27201  lgsdir2lem2  27235  lgsdir2lem3  27236  0reno  28366  ex-fl  30391  siilem1  30795  normlem5  31058  normlem6  31059  norm-ii-i  31081  norm3adifii  31092  cmm2i  31551  mayetes3i  31673  nmopcoadji  32045  mdoc2i  32370  dmdoc2i  32372  dp2lt10  32825  dp2ltsuc  32827  dplti  32846  sqsscirc1  33881  ballotlem1c  34482  hgt750lem  34625  problem5  35652  circum  35657  bj-pinftyccb  37205  bj-minftyccb  37209  poimirlem25  37635  cntotbnd  37786  3lexlogpow5ineq1  42037  3lexlogpow5ineq2  42038  aks4d1p1p2  42053  aks4d1p1p7  42057  posbezout  42083  aks6d1c7lem1  42163  jm2.23  42979  tr3dom  43511  halffl  45288  wallispi  46061  stirlinglem1  46065  fouriersw  46222  sinnpoly  46885