Theorem 3brtr4i 5145

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

Syntax hints:   = wceq 1567   class class class wbr 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114

This theorem is referenced by:  1lt2nq  10957  0lt1sr  11079  declt  12743  decltc  12744  decle  12749  fzennn  14003  faclbnd4lem1  14328  fsumabs  15852  basendxltplusgndx  17338  basendxlttsetndx  17407  basendxltplendx  17421  basendxltdsndx  17440  basendxltunifndx  17450  ovolfiniun  25628  log2ublem3  27078  log2ub  27079  bclbnd  27409  bposlem8  27420  basendxltedgfndx  29284  nmblolbii  31091  normlem6  31407  norm-ii-i  31429  nmbdoplbi  32316  dp2lt  33144  dp2ltsuc  33145  dp2ltc  33146  dplt  33163  dpltc  33166  dpmul4  33173  hgt750lemd  34979  hgt750lem  34982  supxrltinfxr  46054  nnsum4primesevenALTV  48454