Theorem 3brtr4i 5126

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

Syntax hints:   = wceq 1541   class class class wbr 5096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097

This theorem is referenced by:  1lt2nq  10882  0lt1sr  11004  declt  12633  decltc  12634  decle  12639  fzennn  13889  faclbnd4lem1  14214  fsumabs  15722  basendxltplusgndx  17204  basendxlttsetndx  17273  basendxltplendx  17287  basendxltdsndx  17306  basendxltunifndx  17316  ovolfiniun  25456  log2ublem3  26912  log2ub  26913  bclbnd  27245  bposlem8  27256  basendxltedgfndx  29016  nmblolbii  30823  normlem6  31139  norm-ii-i  31161  nmbdoplbi  32048  dp2lt  32915  dp2ltsuc  32916  dp2ltc  32917  dplt  32934  dpltc  32937  dpmul4  32944  hgt750lemd  34754  hgt750lem  34757  supxrltinfxr  45635  nnsum4primesevenALTV  47989