Theorem breqtri 4608

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

Syntax hints:   = wceq 1475   class class class wbr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584

This theorem is referenced by:  breqtrri  4610  3brtr3i  4612  supsrlem  9811  0lt1  10429  le9lt10  11405  9lt10  11549  hashunlei  13072  sqrt2gt1lt2  13863  trireciplem  14433  cos1bnd  14756  cos2bnd  14757  cos01gt0  14760  sin4lt0  14764  rpnnen2lem3  14784  z4even  14946  gcdaddmlem  15083  dec2dvds  15605  abvtrivd  18663  sincos4thpi  24069  log2cnv  24471  log2ublem2  24474  log2ublem3  24475  log2le1  24477  birthday  24481  harmonicbnd3  24534  lgam1  24590  basellem7  24613  ppiublem1  24727  ppiublem2  24728  ppiub  24729  bposlem4  24812  bposlem5  24813  bposlem9  24817  lgsdir2lem2  24851  lgsdir2lem3  24852  ex-fl  26696  siilem1  27090  normlem5  27355  normlem6  27356  norm-ii-i  27378  norm3adifii  27389  cmm2i  27850  mayetes3i  27972  nmopcoadji  28344  mdoc2i  28669  dmdoc2i  28671  sqsscirc1  29282  ballotlem1c  29896  problem5  30817  circum  30822  bj-pinftyccb  32285  bj-minftyccb  32289  poimirlem25  32604  cntotbnd  32765  jm2.23  36581  halffl  38451  wallispi  38963  stirlinglem1  38967  fouriersw  39124