Theorem eqbrtrri 5123

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
eqbrtrr.1	⊢ 𝐴 = 𝐵
eqbrtrr.2	⊢ 𝐴𝑅𝐶

Assertion

Ref	Expression
eqbrtrri	⊢ 𝐵𝑅𝐶

Proof of Theorem eqbrtrri

Step	Hyp	Ref	Expression
1		eqbrtrr.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2771	. 2 ⊢ 𝐵 = 𝐴
3		eqbrtrr.2	. 2 ⊢ 𝐴𝑅𝐶
4	2, 3	eqbrtri 5121	1 ⊢ 𝐵𝑅𝐶

Syntax hints:   = wceq 1560   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  3brtr3i  5129  expnass  14221  faclbnd4lem1  14306  sqrt2gt1lt2  15301  cos1bnd  16219  cos2bnd  16220  prdsvalstr  17481  chnub  18654  ovolre  25584  pigt3  26580  pige3ALT  26582  atan1  26990  log2ublem1  27008  sqrtlim  27034  bposlem8  27352  chebbnd1  27533  norm-ii-i  31337  nmopadji  32290  unierri  32304  ballotlem2  34783  hgt750lemd  34939  hgt750lem  34942  stoweidlem26  46597  wallispilem5  46640