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  25435  log2ublem3  26891  log2ub  26892  bclbnd  27224  bposlem8  27235  basendxltedgfndx  28974  nmblolbii  30778  normlem6  31094  norm-ii-i  31116  nmbdoplbi  32003  dp2lt  32855  dp2ltsuc  32856  dp2ltc  32857  dplt  32874  dpltc  32877  dpmul4  32884  hgt750lemd  34632  hgt750lem  34635  supxrltinfxr  45438  nnsum4primesevenALTV  47795