Theorem breqtri 4913

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

Syntax hints:   = wceq 1601   class class class wbr 4888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4889

This theorem is referenced by:  breqtrri  4915  3brtr3i  4917  supsrlem  10270  0lt1  10900  le9lt10  11878  9lt10  11983  hashunlei  13532  sqrt2gt1lt2  14428  trireciplem  15007  cos1bnd  15328  cos2bnd  15329  cos01gt0  15332  sin4lt0  15336  rpnnen2lem3  15358  z4even  15512  gcdaddmlem  15661  dec2dvds  16182  abvtrivd  19243  sincos4thpi  24714  log2cnv  25134  log2ublem2  25137  log2ublem3  25138  log2le1  25140  birthday  25144  harmonicbnd3  25197  lgam1  25253  basellem7  25276  ppiublem1  25390  ppiublem2  25391  ppiub  25392  bposlem4  25475  bposlem5  25476  bposlem9  25480  lgsdir2lem2  25514  lgsdir2lem3  25515  ex-fl  27896  siilem1  28295  normlem5  28560  normlem6  28561  norm-ii-i  28583  norm3adifii  28594  cmm2i  29055  mayetes3i  29177  nmopcoadji  29549  mdoc2i  29874  dmdoc2i  29876  dp2lt10  30168  dp2ltsuc  30170  dplti  30189  sqsscirc1  30560  ballotlem1c  31176  hgt750lem  31339  problem5  32168  circum  32173  bj-pinftyccb  33706  bj-minftyccb  33710  poimirlem25  34069  cntotbnd  34228  jm2.23  38536  halffl  40433  wallispi  41228  stirlinglem1  41232  fouriersw  41389