Theorem 3brtr4i 5100

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

Syntax hints:   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  1lt2nq  10660  0lt1sr  10782  declt  12394  decltc  12395  decle  12400  fzennn  13616  faclbnd4lem1  13935  fsumabs  15441  basendxltplusgndx  16917  basendxlttsetndx  16990  basendxltplendx  17003  basendxltdsndx  17019  basendxltunifndx  17028  ovolfiniun  24570  log2ublem3  26003  log2ub  26004  bclbnd  26333  bposlem8  26344  baseltedgf  27266  baseltedgfOLD  27267  nmblolbii  29062  normlem6  29378  norm-ii-i  29400  nmbdoplbi  30287  dp2lt  31061  dp2ltsuc  31062  dp2ltc  31063  dplt  31080  dpltc  31083  dpmul4  31090  hgt750lemd  32528  hgt750lem  32531  supxrltinfxr  42879  nnsum4primesevenALTV  45141