Theorem breqtri 4867

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

Syntax hints:   = wceq 1653   class class class wbr 4842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-rab 3097  df-v 3386  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-br 4843

This theorem is referenced by:  breqtrri  4869  3brtr3i  4871  supsrlem  10219  0lt1  10841  le9lt10  11808  9lt10  11913  hashunlei  13458  sqrt2gt1lt2  14353  trireciplem  14929  cos1bnd  15250  cos2bnd  15251  cos01gt0  15254  sin4lt0  15258  rpnnen2lem3  15278  z4even  15441  gcdaddmlem  15577  dec2dvds  16097  abvtrivd  19155  sincos4thpi  24604  log2cnv  25020  log2ublem2  25023  log2ublem3  25024  log2le1  25026  birthday  25030  harmonicbnd3  25083  lgam1  25139  basellem7  25162  ppiublem1  25276  ppiublem2  25277  ppiub  25278  bposlem4  25361  bposlem5  25362  bposlem9  25366  lgsdir2lem2  25400  lgsdir2lem3  25401  ex-fl  27825  siilem1  28224  normlem5  28489  normlem6  28490  norm-ii-i  28512  norm3adifii  28523  cmm2i  28984  mayetes3i  29106  nmopcoadji  29478  mdoc2i  29803  dmdoc2i  29805  dp2lt10  30101  dp2ltsuc  30103  dplti  30122  sqsscirc1  30463  ballotlem1c  31079  hgt750lem  31242  problem5  32071  circum  32076  bj-pinftyccb  33600  bj-minftyccb  33604  poimirlem25  33916  cntotbnd  34075  jm2.23  38337  halffl  40244  wallispi  41019  stirlinglem1  41023  fouriersw  41180