Theorem 3brtr4i 5122

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 11-Aug-1999.)

Hypotheses

Ref	Expression
3brtr4.1	⊢ 𝐴𝑅𝐵
3brtr4.2	⊢ 𝐶 = 𝐴
3brtr4.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3brtr4i	⊢ 𝐶𝑅𝐷

Proof of Theorem 3brtr4i

Step	Hyp	Ref	Expression
1		3brtr4.2	. . 3 ⊢ 𝐶 = 𝐴
2		3brtr4.1	. . 3 ⊢ 𝐴𝑅𝐵
3	1, 2	eqbrtri 5113	. 2 ⊢ 𝐶𝑅𝐵
4		3brtr4.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	breqtrri 5119	1 ⊢ 𝐶𝑅𝐷

Syntax hints:   = wceq 1540   class class class wbr 5092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  1lt2nq  10867  0lt1sr  10989  declt  12619  decltc  12620  decle  12625  fzennn  13875  faclbnd4lem1  14200  fsumabs  15708  basendxltplusgndx  17190  basendxlttsetndx  17259  basendxltplendx  17273  basendxltdsndx  17292  basendxltunifndx  17302  ovolfiniun  25400  log2ublem3  26856  log2ub  26857  bclbnd  27189  bposlem8  27200  basendxltedgfndx  28939  nmblolbii  30743  normlem6  31059  norm-ii-i  31081  nmbdoplbi  31968  dp2lt  32825  dp2ltsuc  32826  dp2ltc  32827  dplt  32844  dpltc  32847  dpmul4  32854  hgt750lemd  34616  hgt750lem  34619  supxrltinfxr  45432  nnsum4primesevenALTV  47789