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 232	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1562   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 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  breqtrri  5129  3brtr3i  5131  supsrlem  11071  0lt1  11711  le9lt10  12722  9lt10  12827  hashunlei  14440  sqrt2gt1lt2  15303  trireciplem  15894  cos1bnd  16221  cos2bnd  16222  cos01gt0  16225  sin4lt0  16229  rpnnen2lem3  16250  z4even  16408  gcdaddmlem  16560  dec2dvds  17101  abvtrivd  20883  sincos4thpi  26580  log2cnv  27011  log2ublem2  27014  log2ublem3  27015  log2le1  27017  birthday  27021  harmonicbnd3  27074  lgam1  27130  basellem7  27153  ppiublem1  27268  ppiub  27270  bposlem4  27353  bposlem5  27354  bposlem9  27358  lgsdir2lem2  27392  lgsdir2lem3  27393  1reno  28592  ex-fl  30651  siilem1  31056  normlem5  31319  normlem6  31320  norm-ii-i  31342  norm3adifii  31353  cmm2i  31812  mayetes3i  31934  nmopcoadji  32306  mdoc2i  32631  dmdoc2i  32633  dp2lt10  33063  dp2ltsuc  33065  dplti  33084  sqsscirc1  34207  ballotlem1c  34807  hgt750lem  34947  problem5  36024  circum  36029  bj-pinftyccb  37718  bj-minftyccb  37722  poimirlem25  38149  cntotbnd  38300  3lexlogpow5ineq1  42676  3lexlogpow5ineq2  42677  aks4d1p1p2  42692  aks4d1p1p7  42696  posbezout  42722  aks6d1c7lem1  42802  jm2.23  43578  tr3dom  44109  halffl  45880  wallispi  46649  stirlinglem1  46653  fouriersw  46810  sinnpoly  47490