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 1560   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 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  1lt2nq  10931  0lt1sr  11053  declt  12721  decltc  12722  decle  12727  fzennn  13981  faclbnd4lem1  14306  fsumabs  15829  basendxltplusgndx  17315  basendxlttsetndx  17384  basendxltplendx  17398  basendxltdsndx  17417  basendxltunifndx  17427  ovolfiniun  25563  log2ublem3  27013  log2ub  27014  bclbnd  27344  bposlem8  27355  basendxltedgfndx  29195  nmblolbii  31002  normlem6  31318  norm-ii-i  31340  nmbdoplbi  32227  dp2lt  33062  dp2ltsuc  33063  dp2ltc  33064  dplt  33081  dpltc  33084  dpmul4  33091  hgt750lemd  34942  hgt750lem  34945  supxrltinfxr  46023  nnsum4primesevenALTV  48423