Theorem 3brtr4i 5141

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

Syntax hints:   = wceq 1570   class class class wbr 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is referenced by:  1lt2nq  10953  0lt1sr  11075  declt  12739  decltc  12740  decle  12745  fzennn  14000  faclbnd4lem1  14325  fsumabs  15849  basendxltplusgndx  17334  basendxlttsetndx  17403  basendxltplendx  17417  basendxltdsndx  17436  basendxltunifndx  17446  ovolfiniun  25660  log2ublem3  27113  log2ub  27114  bclbnd  27444  bposlem8  27455  basendxltedgfndx  29344  nmblolbii  31151  normlem6  31467  norm-ii-i  31489  nmbdoplbi  32376  dp2lt  33204  dp2ltsuc  33205  dp2ltc  33206  dplt  33223  dpltc  33226  dpmul4  33233  hgt750lemd  35035  hgt750lem  35038  supxrltinfxr  46183  nnsum4primesevenALTV  48586