Theorem breqtri 5130

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

This proof depends on syntax axioms:   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  breqtrri  5132  3brtr3i  5134  supsrlem  11123  0lt1  11763  le9lt10  12771  9lt10  12876  hashunlei  14493  sqrt2gt1lt2  15364  trireciplem  15954  cos1bnd  16278  cos2bnd  16279  cos01gt0  16282  sin4lt0  16286  rpnnen2lem3  16307  z4even  16465  gcdaddmlem  16617  dec2dvds  17158  abvtrivd  21001  sincos4thpi  26754  log2cnv  27184  log2ublem2  27187  log2ublem3  27188  log2le1  27190  birthday  27194  harmonicbnd3  27247  lgam1  27303  basellem7  27326  ppiublem1  27441  ppiub  27443  bposlem4  27526  bposlem5  27527  bposlem9  27531  lgsdir2lem2  27565  lgsdir2lem3  27566  1reno  28765  ex-fl  30930  siilem1  31335  normlem5  31598  normlem6  31599  norm-ii-i  31621  norm3adifii  31632  cmm2i  32091  mayetes3i  32213  nmopcoadji  32585  mdoc2i  32910  dmdoc2i  32912  dp2lt10  33332  dp2ltsuc  33334  dplti  33353  sqsscirc1  34421  ballotlem1c  35022  hgt750lem  35162  problem5  36251  circum  36256  bj-pinftyccb  37976  bj-minftyccb  37980  poimirlem25  38397  cntotbnd  38549  3lexlogpow5ineq1  42923  3lexlogpow5ineq2  42924  aks4d1p1p2  42939  aks4d1p1p7  42943  posbezout  42969  aks6d1c7lem1  43049  jm2.23  43840  tr3dom  44371  halffl  46132  wallispi  46901  stirlinglem1  46905  fouriersw  47062  goldratval  47757