Theorem 3brtr4i 5140

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

Syntax hints:   = wceq 1540   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  1lt2nq  10933  0lt1sr  11055  declt  12684  decltc  12685  decle  12690  fzennn  13940  faclbnd4lem1  14265  fsumabs  15774  basendxltplusgndx  17256  basendxlttsetndx  17325  basendxltplendx  17339  basendxltdsndx  17358  basendxltunifndx  17368  ovolfiniun  25409  log2ublem3  26865  log2ub  26866  bclbnd  27198  bposlem8  27209  basendxltedgfndx  28928  nmblolbii  30735  normlem6  31051  norm-ii-i  31073  nmbdoplbi  31960  dp2lt  32812  dp2ltsuc  32813  dp2ltc  32814  dplt  32831  dpltc  32834  dpmul4  32841  hgt750lemd  34646  hgt750lem  34649  supxrltinfxr  45452  nnsum4primesevenALTV  47806