Theorem breqtri 5173

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

Syntax hints:   = wceq 1541   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  breqtrri  5175  3brtr3i  5177  supsrlem  11108  0lt1  11740  le9lt10  12708  9lt10  12812  hashunlei  14389  sqrt2gt1lt2  15225  trireciplem  15812  cos1bnd  16134  cos2bnd  16135  cos01gt0  16138  sin4lt0  16142  rpnnen2lem3  16163  z4even  16319  gcdaddmlem  16469  dec2dvds  17000  abvtrivd  20591  sincos4thpi  26247  log2cnv  26673  log2ublem2  26676  log2ublem3  26677  log2le1  26679  birthday  26683  harmonicbnd3  26736  lgam1  26792  basellem7  26815  ppiublem1  26929  ppiub  26931  bposlem4  27014  bposlem5  27015  bposlem9  27019  lgsdir2lem2  27053  lgsdir2lem3  27054  ex-fl  29955  siilem1  30359  normlem5  30622  normlem6  30623  norm-ii-i  30645  norm3adifii  30656  cmm2i  31115  mayetes3i  31237  nmopcoadji  31609  mdoc2i  31934  dmdoc2i  31936  dp2lt10  32305  dp2ltsuc  32307  dplti  32326  sqsscirc1  33174  ballotlem1c  33792  hgt750lem  33949  problem5  34940  circum  34945  bj-pinftyccb  36405  bj-minftyccb  36409  poimirlem25  36816  cntotbnd  36967  3lexlogpow5ineq1  41225  3lexlogpow5ineq2  41226  aks4d1p1p2  41241  aks4d1p1p7  41245  jm2.23  42037  tr3dom  42581  halffl  44305  wallispi  45085  stirlinglem1  45089  fouriersw  45246