Theorem 3brtr4i 5134

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

This proof depends on syntax axioms:   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103

This theorem is used by:  1lt2nq  11065  0lt1sr  11187  declt  12854  decltc  12855  decle  12860  fzennn  14118  faclbnd4lem1  14444  fsumabs  15977  basendxltplusgndx  17466  basendxlttsetndx  17535  basendxltplendx  17549  basendxltdsndx  17568  basendxltunifndx  17578  ovolfiniun  25831  log2ublem3  27285  log2ub  27286  bclbnd  27616  bposlem8  27627  basendxltedgfndx  29581  nmblolbii  31410  normlem6  31726  norm-ii-i  31748  nmbdoplbi  32635  dp2lt  33501  dp2ltsuc  33502  dp2ltc  33503  dplt  33520  dpltc  33523  dpmul4  33530  hgt750lemd  35327  hgt750lem  35330  supxrltinfxr  46595  goldratval  48072  nnsum4primesevenALTV  49035