Theorem 3brtr4i 5132

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

Syntax hints:   = wceq 1540   class class class wbr 5102

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  1lt2nq  10902  0lt1sr  11024  declt  12653  decltc  12654  decle  12659  fzennn  13909  faclbnd4lem1  14234  fsumabs  15743  basendxltplusgndx  17225  basendxlttsetndx  17294  basendxltplendx  17308  basendxltdsndx  17327  basendxltunifndx  17337  ovolfiniun  25378  log2ublem3  26834  log2ub  26835  bclbnd  27167  bposlem8  27178  basendxltedgfndx  28897  nmblolbii  30701  normlem6  31017  norm-ii-i  31039  nmbdoplbi  31926  dp2lt  32778  dp2ltsuc  32779  dp2ltc  32780  dplt  32797  dpltc  32800  dpmul4  32807  hgt750lemd  34612  hgt750lem  34615  supxrltinfxr  45418  nnsum4primesevenALTV  47775