Theorem 3brtr4i 5104

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

Syntax hints:   = wceq 1539   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075

This theorem is referenced by:  1lt2nq  10729  0lt1sr  10851  declt  12465  decltc  12466  decle  12471  fzennn  13688  faclbnd4lem1  14007  fsumabs  15513  basendxltplusgndx  16991  basendxlttsetndx  17065  basendxltplendx  17079  basendxltdsndx  17098  basendxltunifndx  17108  ovolfiniun  24665  log2ublem3  26098  log2ub  26099  bclbnd  26428  bposlem8  26439  basendxltedgfndx  27363  baseltedgfOLD  27364  nmblolbii  29161  normlem6  29477  norm-ii-i  29499  nmbdoplbi  30386  dp2lt  31159  dp2ltsuc  31160  dp2ltc  31161  dplt  31178  dpltc  31181  dpmul4  31188  hgt750lemd  32628  hgt750lem  32631  supxrltinfxr  42989  nnsum4primesevenALTV  45253