Theorem 3brtr4i 4905

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

Syntax hints:   = wceq 1656   class class class wbr 4875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-br 4876

This theorem is referenced by:  1lt2nq  10117  0lt1sr  10239  declt  11857  decltc  11858  decle  11863  fzennn  13069  faclbnd4lem1  13380  fsumabs  14914  ovolfiniun  23674  log2ublem3  25095  log2ub  25096  emgt0  25153  bclbnd  25425  bposlem8  25436  baseltedgf  26299  nmblolbii  28205  normlem6  28523  norm-ii-i  28545  nmbdoplbi  29434  dp2lt  30134  dp2ltsuc  30135  dp2ltc  30136  dplt  30153  dpltc  30156  dpmul4  30163  hgt750lemd  31271  hgt750lem  31274  supxrltinfxr  40470  nnsum4primesevenALTV  42537