Theorem 3brtr4i 5174

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 5165	. 2 ⊢ 𝐶𝑅𝐵
4		3brtr4.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	breqtrri 5171	1 ⊢ 𝐶𝑅𝐷

Syntax hints:   = wceq 1542   class class class wbr 5144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5145

This theorem is referenced by:  1lt2nq  10955  0lt1sr  11077  declt  12692  decltc  12693  decle  12698  fzennn  13920  faclbnd4lem1  14240  fsumabs  15734  basendxltplusgndx  17213  basendxlttsetndx  17287  basendxltplendx  17301  basendxltdsndx  17320  basendxltunifndx  17330  ovolfiniun  24987  log2ublem3  26420  log2ub  26421  bclbnd  26750  bposlem8  26761  basendxltedgfndx  28220  baseltedgfOLD  28221  nmblolbii  30017  normlem6  30333  norm-ii-i  30355  nmbdoplbi  31242  dp2lt  32022  dp2ltsuc  32023  dp2ltc  32024  dplt  32041  dpltc  32044  dpmul4  32051  hgt750lemd  33591  hgt750lem  33594  supxrltinfxr  44032  nnsum4primesevenALTV  46342