Theorem 3brtr4i 5128

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

Syntax hints:   = wceq 1541   class class class wbr 5098

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  1lt2nq  10884  0lt1sr  11006  declt  12635  decltc  12636  decle  12641  fzennn  13891  faclbnd4lem1  14216  fsumabs  15724  basendxltplusgndx  17206  basendxlttsetndx  17275  basendxltplendx  17289  basendxltdsndx  17308  basendxltunifndx  17318  ovolfiniun  25458  log2ublem3  26914  log2ub  26915  bclbnd  27247  bposlem8  27258  basendxltedgfndx  29067  nmblolbii  30874  normlem6  31190  norm-ii-i  31212  nmbdoplbi  32099  dp2lt  32966  dp2ltsuc  32967  dp2ltc  32968  dplt  32985  dpltc  32988  dpmul4  32995  hgt750lemd  34805  hgt750lem  34808  supxrltinfxr  45693  nnsum4primesevenALTV  48047