Theorem breqtri 5132

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

Syntax hints:   = wceq 1540   class class class wbr 5107

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  breqtrri  5134  3brtr3i  5136  supsrlem  11064  0lt1  11700  le9lt10  12676  9lt10  12780  hashunlei  14390  sqrt2gt1lt2  15240  trireciplem  15828  cos1bnd  16155  cos2bnd  16156  cos01gt0  16159  sin4lt0  16163  rpnnen2lem3  16184  z4even  16342  gcdaddmlem  16494  dec2dvds  17034  abvtrivd  20741  sincos4thpi  26422  log2cnv  26854  log2ublem2  26857  log2ublem3  26858  log2le1  26860  birthday  26864  harmonicbnd3  26918  lgam1  26974  basellem7  26997  ppiublem1  27113  ppiub  27115  bposlem4  27198  bposlem5  27199  bposlem9  27203  lgsdir2lem2  27237  lgsdir2lem3  27238  0reno  28348  ex-fl  30376  siilem1  30780  normlem5  31043  normlem6  31044  norm-ii-i  31066  norm3adifii  31077  cmm2i  31536  mayetes3i  31658  nmopcoadji  32030  mdoc2i  32355  dmdoc2i  32357  dp2lt10  32804  dp2ltsuc  32806  dplti  32825  sqsscirc1  33898  ballotlem1c  34499  hgt750lem  34642  problem5  35656  circum  35661  bj-pinftyccb  37209  bj-minftyccb  37213  poimirlem25  37639  cntotbnd  37790  3lexlogpow5ineq1  42042  3lexlogpow5ineq2  42043  aks4d1p1p2  42058  aks4d1p1p7  42062  posbezout  42088  aks6d1c7lem1  42168  jm2.23  42985  tr3dom  43517  halffl  45294  wallispi  46068  stirlinglem1  46072  fouriersw  46229  sinnpoly  46892