Theorem 3brtr4i 5135

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

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

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  1lt2nq  11058  0lt1sr  11180  declt  12847  decltc  12848  decle  12853  fzennn  14111  faclbnd4lem1  14437  fsumabs  15968  basendxltplusgndx  17457  basendxlttsetndx  17526  basendxltplendx  17540  basendxltdsndx  17559  basendxltunifndx  17569  ovolfiniun  25822  log2ublem3  27276  log2ub  27277  bclbnd  27607  bposlem8  27618  basendxltedgfndx  29572  nmblolbii  31401  normlem6  31717  norm-ii-i  31739  nmbdoplbi  32626  dp2lt  33451  dp2ltsuc  33452  dp2ltc  33453  dplt  33470  dpltc  33473  dpmul4  33480  hgt750lemd  35277  hgt750lem  35280  supxrltinfxr  46458  goldratval  47935  nnsum4primesevenALTV  48898