Theorem 3brtr4i 5177

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

Syntax hints:   = wceq 1541   class class class wbr 5147

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  1lt2nq  10964  0lt1sr  11086  declt  12701  decltc  12702  decle  12707  fzennn  13929  faclbnd4lem1  14249  fsumabs  15743  basendxltplusgndx  17222  basendxlttsetndx  17296  basendxltplendx  17310  basendxltdsndx  17329  basendxltunifndx  17339  ovolfiniun  25009  log2ublem3  26442  log2ub  26443  bclbnd  26772  bposlem8  26783  basendxltedgfndx  28242  baseltedgfOLD  28243  nmblolbii  30039  normlem6  30355  norm-ii-i  30377  nmbdoplbi  31264  dp2lt  32038  dp2ltsuc  32039  dp2ltc  32040  dplt  32057  dpltc  32060  dpmul4  32067  hgt750lemd  33648  hgt750lem  33651  supxrltinfxr  44145  nnsum4primesevenALTV  46455