Theorem 3brtr4i 5125

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

Syntax hints:   = wceq 1541   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  1lt2nq  10874  0lt1sr  10996  declt  12626  decltc  12627  decle  12632  fzennn  13885  faclbnd4lem1  14210  fsumabs  15718  basendxltplusgndx  17200  basendxlttsetndx  17269  basendxltplendx  17283  basendxltdsndx  17302  basendxltunifndx  17312  ovolfiniun  25439  log2ublem3  26895  log2ub  26896  bclbnd  27228  bposlem8  27239  basendxltedgfndx  28983  nmblolbii  30790  normlem6  31106  norm-ii-i  31128  nmbdoplbi  32015  dp2lt  32876  dp2ltsuc  32877  dp2ltc  32878  dplt  32895  dpltc  32898  dpmul4  32905  hgt750lemd  34672  hgt750lem  34675  supxrltinfxr  45561  nnsum4primesevenALTV  47915