Theorem breqtri 5093

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

Syntax hints:   = wceq 1537   class class class wbr 5068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069

This theorem is referenced by:  breqtrri  5095  3brtr3i  5097  supsrlem  10535  0lt1  11164  le9lt10  12128  9lt10  12232  hashunlei  13789  sqrt2gt1lt2  14636  trireciplem  15219  cos1bnd  15542  cos2bnd  15543  cos01gt0  15546  sin4lt0  15550  rpnnen2lem3  15571  z4even  15725  gcdaddmlem  15874  dec2dvds  16401  abvtrivd  19613  sincos4thpi  25101  log2cnv  25524  log2ublem2  25527  log2ublem3  25528  log2le1  25530  birthday  25534  harmonicbnd3  25587  lgam1  25643  basellem7  25666  ppiublem1  25780  ppiub  25782  bposlem4  25865  bposlem5  25866  bposlem9  25870  lgsdir2lem2  25904  lgsdir2lem3  25905  ex-fl  28228  siilem1  28630  normlem5  28893  normlem6  28894  norm-ii-i  28916  norm3adifii  28927  cmm2i  29386  mayetes3i  29508  nmopcoadji  29880  mdoc2i  30205  dmdoc2i  30207  dp2lt10  30562  dp2ltsuc  30564  dplti  30583  sqsscirc1  31153  ballotlem1c  31767  hgt750lem  31924  problem5  32914  circum  32919  bj-pinftyccb  34505  bj-minftyccb  34509  poimirlem25  34919  cntotbnd  35076  jm2.23  39600  tr3dom  39901  halffl  41570  wallispi  42362  stirlinglem1  42366  fouriersw  42523