Theorem 3brtr4i 5143

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

This proof depends on syntax axioms:   = wceq 1570   class class class wbr 5111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112

This theorem is used by:  1lt2nq  10975  0lt1sr  11097  declt  12762  decltc  12763  decle  12768  fzennn  14024  faclbnd4lem1  14349  fsumabs  15878  basendxltplusgndx  17363  basendxlttsetndx  17432  basendxltplendx  17446  basendxltdsndx  17465  basendxltunifndx  17475  ovolfiniun  25713  log2ublem3  27166  log2ub  27167  bclbnd  27497  bposlem8  27508  basendxltedgfndx  29401  nmblolbii  31224  normlem6  31540  norm-ii-i  31562  nmbdoplbi  32449  dp2lt  33276  dp2ltsuc  33277  dp2ltc  33278  dplt  33295  dpltc  33298  dpmul4  33305  hgt750lemd  35102  hgt750lem  35105  supxrltinfxr  46223  nnsum4primesevenALTV  48626