Theorem 3brtr4i 5178

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

Syntax hints:   = wceq 1534   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149

This theorem is referenced by:  1lt2nq  10997  0lt1sr  11119  declt  12736  decltc  12737  decle  12742  fzennn  13966  faclbnd4lem1  14285  fsumabs  15780  basendxltplusgndx  17262  basendxlttsetndx  17336  basendxltplendx  17350  basendxltdsndx  17369  basendxltunifndx  17379  ovolfiniun  25443  log2ublem3  26893  log2ub  26894  bclbnd  27226  bposlem8  27237  basendxltedgfndx  28819  baseltedgfOLD  28820  nmblolbii  30622  normlem6  30938  norm-ii-i  30960  nmbdoplbi  31847  dp2lt  32621  dp2ltsuc  32622  dp2ltc  32623  dplt  32640  dpltc  32643  dpmul4  32650  hgt750lemd  34280  hgt750lem  34283  supxrltinfxr  44831  nnsum4primesevenALTV  47141