Theorem 3brtr4i 5130

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

Syntax hints:   = wceq 1542   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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  1lt2nq  10896  0lt1sr  11018  declt  12647  decltc  12648  decle  12653  fzennn  13903  faclbnd4lem1  14228  fsumabs  15736  basendxltplusgndx  17218  basendxlttsetndx  17287  basendxltplendx  17301  basendxltdsndx  17320  basendxltunifndx  17330  ovolfiniun  25470  log2ublem3  26926  log2ub  26927  bclbnd  27259  bposlem8  27270  basendxltedgfndx  29079  nmblolbii  30887  normlem6  31203  norm-ii-i  31225  nmbdoplbi  32112  dp2lt  32977  dp2ltsuc  32978  dp2ltc  32979  dplt  32996  dpltc  32999  dpmul4  33006  hgt750lemd  34826  hgt750lem  34829  supxrltinfxr  45807  nnsum4primesevenALTV  48161