Theorem breqtri 5138

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112

This theorem is used by:  breqtrri  5140  3brtr3i  5142  supsrlem  11115  0lt1  11755  le9lt10  12763  9lt10  12868  hashunlei  14484  sqrt2gt1lt2  15353  trireciplem  15943  cos1bnd  16269  cos2bnd  16270  cos01gt0  16273  sin4lt0  16277  rpnnen2lem3  16298  z4even  16456  gcdaddmlem  16608  dec2dvds  17149  abvtrivd  20989  sincos4thpi  26733  log2cnv  27164  log2ublem2  27167  log2ublem3  27168  log2le1  27170  birthday  27174  harmonicbnd3  27227  lgam1  27283  basellem7  27306  ppiublem1  27421  ppiub  27423  bposlem4  27506  bposlem5  27507  bposlem9  27511  lgsdir2lem2  27545  lgsdir2lem3  27546  1reno  28745  ex-fl  30873  siilem1  31278  normlem5  31541  normlem6  31542  norm-ii-i  31564  norm3adifii  31575  cmm2i  32034  mayetes3i  32156  nmopcoadji  32528  mdoc2i  32853  dmdoc2i  32855  dp2lt10  33277  dp2ltsuc  33279  dplti  33298  sqsscirc1  34366  ballotlem1c  34967  hgt750lem  35107  problem5  36202  circum  36207  bj-pinftyccb  37926  bj-minftyccb  37930  poimirlem25  38357  cntotbnd  38509  3lexlogpow5ineq1  42883  3lexlogpow5ineq2  42884  aks4d1p1p2  42899  aks4d1p1p7  42903  posbezout  42929  aks6d1c7lem1  43009  jm2.23  43800  tr3dom  44331  halffl  46092  wallispi  46861  stirlinglem1  46865  fouriersw  47022  sinnpoly  47705