Theorem 3brtr4i 4816

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

Syntax hints:   = wceq 1631   class class class wbr 4786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787

This theorem is referenced by:  1lt2nq  9997  0lt1sr  10118  declt  11732  decltOLD  11733  decltc  11734  decltcOLD  11735  decle  11742  decleOLD  11745  fzennn  12975  faclbnd4lem1  13284  fsumabs  14740  ovolfiniun  23489  log2ublem3  24896  log2ub  24897  emgt0  24954  bclbnd  25226  bposlem8  25237  baseltedgf  26093  nmblolbii  27994  normlem6  28312  norm-ii-i  28334  nmbdoplbi  29223  dp2lt  29932  dp2ltsuc  29933  dp2ltc  29934  dplt  29952  dpltc  29955  dpmul4  29962  hgt750lemd  31066  hgt750lem  31069  supxrltinfxr  40193  nnsum4primesevenALTV  42217