Theorem breqtri 5110

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

Syntax hints:   = wceq 1542   class class class wbr 5085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  breqtrri  5112  3brtr3i  5114  supsrlem  11034  0lt1  11672  le9lt10  12671  9lt10  12775  hashunlei  14387  sqrt2gt1lt2  15236  trireciplem  15827  cos1bnd  16154  cos2bnd  16155  cos01gt0  16158  sin4lt0  16162  rpnnen2lem3  16183  z4even  16341  gcdaddmlem  16493  dec2dvds  17034  abvtrivd  20809  sincos4thpi  26477  log2cnv  26908  log2ublem2  26911  log2ublem3  26912  log2le1  26914  birthday  26918  harmonicbnd3  26971  lgam1  27027  basellem7  27050  ppiublem1  27165  ppiub  27167  bposlem4  27250  bposlem5  27251  bposlem9  27255  lgsdir2lem2  27289  lgsdir2lem3  27290  1reno  28489  ex-fl  30517  siilem1  30922  normlem5  31185  normlem6  31186  norm-ii-i  31208  norm3adifii  31219  cmm2i  31678  mayetes3i  31800  nmopcoadji  32172  mdoc2i  32497  dmdoc2i  32499  dp2lt10  32943  dp2ltsuc  32945  dplti  32964  sqsscirc1  34052  ballotlem1c  34652  hgt750lem  34795  problem5  35851  circum  35856  bj-pinftyccb  37535  bj-minftyccb  37539  poimirlem25  37966  cntotbnd  38117  3lexlogpow5ineq1  42493  3lexlogpow5ineq2  42494  aks4d1p1p2  42509  aks4d1p1p7  42513  posbezout  42539  aks6d1c7lem1  42619  jm2.23  43424  tr3dom  43955  halffl  45729  wallispi  46498  stirlinglem1  46502  fouriersw  46659  sinnpoly  47339