Theorem breqtri 5140

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

Syntax hints:   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  breqtrri  5142  3brtr3i  5144  supsrlem  11096  0lt1  11736  le9lt10  12743  9lt10  12848  hashunlei  14462  sqrt2gt1lt2  15325  trireciplem  15916  cos1bnd  16243  cos2bnd  16244  cos01gt0  16247  sin4lt0  16251  rpnnen2lem3  16272  z4even  16430  gcdaddmlem  16582  dec2dvds  17123  abvtrivd  20913  sincos4thpi  26644  log2cnv  27075  log2ublem2  27078  log2ublem3  27079  log2le1  27081  birthday  27085  harmonicbnd3  27138  lgam1  27194  basellem7  27217  ppiublem1  27332  ppiub  27334  bposlem4  27417  bposlem5  27418  bposlem9  27422  lgsdir2lem2  27456  lgsdir2lem3  27457  1reno  28656  ex-fl  30739  siilem1  31144  normlem5  31407  normlem6  31408  norm-ii-i  31430  norm3adifii  31441  cmm2i  31900  mayetes3i  32022  nmopcoadji  32394  mdoc2i  32719  dmdoc2i  32721  dp2lt10  33144  dp2ltsuc  33146  dplti  33165  sqsscirc1  34243  ballotlem1c  34843  hgt750lem  34983  problem5  36094  circum  36099  bj-pinftyccb  37787  bj-minftyccb  37791  poimirlem25  38218  cntotbnd  38369  3lexlogpow5ineq1  42745  3lexlogpow5ineq2  42746  aks4d1p1p2  42761  aks4d1p1p7  42765  posbezout  42791  aks6d1c7lem1  42871  jm2.23  43649  tr3dom  44180  halffl  45941  wallispi  46710  stirlinglem1  46714  fouriersw  46871  sinnpoly  47551