Theorem breqtri 5114

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

Syntax hints:   = wceq 1541   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  breqtrri  5116  3brtr3i  5118  supsrlem  11002  0lt1  11639  le9lt10  12615  9lt10  12719  hashunlei  14332  sqrt2gt1lt2  15181  trireciplem  15769  cos1bnd  16096  cos2bnd  16097  cos01gt0  16100  sin4lt0  16104  rpnnen2lem3  16125  z4even  16283  gcdaddmlem  16435  dec2dvds  16975  abvtrivd  20747  sincos4thpi  26449  log2cnv  26881  log2ublem2  26884  log2ublem3  26885  log2le1  26887  birthday  26891  harmonicbnd3  26945  lgam1  27001  basellem7  27024  ppiublem1  27140  ppiub  27142  bposlem4  27225  bposlem5  27226  bposlem9  27230  lgsdir2lem2  27264  lgsdir2lem3  27265  0reno  28399  ex-fl  30427  siilem1  30831  normlem5  31094  normlem6  31095  norm-ii-i  31117  norm3adifii  31128  cmm2i  31587  mayetes3i  31709  nmopcoadji  32081  mdoc2i  32406  dmdoc2i  32408  dp2lt10  32864  dp2ltsuc  32866  dplti  32885  sqsscirc1  33921  ballotlem1c  34521  hgt750lem  34664  problem5  35713  circum  35718  bj-pinftyccb  37265  bj-minftyccb  37269  poimirlem25  37695  cntotbnd  37846  3lexlogpow5ineq1  42157  3lexlogpow5ineq2  42158  aks4d1p1p2  42173  aks4d1p1p7  42177  posbezout  42203  aks6d1c7lem1  42283  jm2.23  43099  tr3dom  43631  halffl  45407  wallispi  46178  stirlinglem1  46182  fouriersw  46339  sinnpoly  47001