Theorem 3brtr4i 5135

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

This proof depends on syntax axioms:   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  1lt2nq  10983  0lt1sr  11105  declt  12770  decltc  12771  decle  12776  fzennn  14033  faclbnd4lem1  14358  fsumabs  15889  basendxltplusgndx  17372  basendxlttsetndx  17441  basendxltplendx  17455  basendxltdsndx  17474  basendxltunifndx  17484  ovolfiniun  25730  log2ublem3  27186  log2ub  27187  bclbnd  27517  bposlem8  27528  basendxltedgfndx  29452  nmblolbii  31281  normlem6  31597  norm-ii-i  31619  nmbdoplbi  32506  dp2lt  33331  dp2ltsuc  33332  dp2ltc  33333  dplt  33350  dpltc  33353  dpmul4  33360  hgt750lemd  35157  hgt750lem  35160  supxrltinfxr  46278  goldratval  47755  nnsum4primesevenALTV  48718