Theorem 3brtr4i 5149

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

Syntax hints:   = wceq 1540   class class class wbr 5119

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  1lt2nq  10985  0lt1sr  11107  declt  12734  decltc  12735  decle  12740  fzennn  13984  faclbnd4lem1  14309  fsumabs  15815  basendxltplusgndx  17298  basendxlttsetndx  17367  basendxltplendx  17381  basendxltdsndx  17400  basendxltunifndx  17410  ovolfiniun  25452  log2ublem3  26908  log2ub  26909  bclbnd  27241  bposlem8  27252  basendxltedgfndx  28919  nmblolbii  30726  normlem6  31042  norm-ii-i  31064  nmbdoplbi  31951  dp2lt  32805  dp2ltsuc  32806  dp2ltc  32807  dplt  32824  dpltc  32827  dpmul4  32834  hgt750lemd  34626  hgt750lem  34629  supxrltinfxr  45424  nnsum4primesevenALTV  47763