Theorem 3brtr4i 5177

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

Syntax hints:   = wceq 1536   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  1lt2nq  11010  0lt1sr  11132  declt  12758  decltc  12759  decle  12764  fzennn  14005  faclbnd4lem1  14328  fsumabs  15833  basendxltplusgndx  17326  basendxlttsetndx  17400  basendxltplendx  17414  basendxltdsndx  17433  basendxltunifndx  17443  ovolfiniun  25549  log2ublem3  27005  log2ub  27006  bclbnd  27338  bposlem8  27349  basendxltedgfndx  29024  baseltedgfOLD  29025  nmblolbii  30827  normlem6  31143  norm-ii-i  31165  nmbdoplbi  32052  dp2lt  32851  dp2ltsuc  32852  dp2ltc  32853  dplt  32870  dpltc  32873  dpmul4  32880  hgt750lemd  34641  hgt750lem  34644  supxrltinfxr  45398  nnsum4primesevenALTV  47725