Theorem 3brtr4i 5178

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 5169	. 2 ⊢ 𝐶𝑅𝐵
4		3brtr4.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	breqtrri 5175	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:  1lt2nq  10970  0lt1sr  11092  declt  12709  decltc  12710  decle  12715  fzennn  13937  faclbnd4lem1  14257  fsumabs  15751  basendxltplusgndx  17230  basendxlttsetndx  17304  basendxltplendx  17318  basendxltdsndx  17337  basendxltunifndx  17347  ovolfiniun  25242  log2ublem3  26677  log2ub  26678  bclbnd  27007  bposlem8  27018  basendxltedgfndx  28508  baseltedgfOLD  28509  nmblolbii  30307  normlem6  30623  norm-ii-i  30645  nmbdoplbi  31532  dp2lt  32306  dp2ltsuc  32307  dp2ltc  32308  dplt  32325  dpltc  32328  dpmul4  32335  hgt750lemd  33946  hgt750lem  33949  supxrltinfxr  44458  nnsum4primesevenALTV  46768