Theorem 3brtr4 2638

Description: Substitution of equality into both sides of a binary relation.

Hypotheses

Ref	Expression
3brtr4.1	|- ARB
3brtr4.2	|- C = A
3brtr4.3	|- D = B

Assertion

Ref	Expression
3brtr4	|- CRD

Proof of Theorem 3brtr4

Step	Hyp	Ref	Expression
1		3brtr4.2	. . 3 |- C = A
2		3brtr4.1	. . 3 |- ARB
3	1, 2	eqbrtr 2629	. 2 |- CRB
4		3brtr4.3	. 2 |- D = B
5	3, 4	breqtrr 2635	1 |- CRD

Syntax hints:   = wceq 954   class class class wbr 2614

This theorem is referenced by:  1sdom2 4511  cda1en 4906  cdacomen 4909  cdaassen 4910  xpcdaen 4911  1lt2pq 5058  0lt1sr 5184  nneo 6152  sqrlem2 6612  sqrlem11 6621  sqrlem16 6626  abstri 6837  faclbnd4lem1 6893  ser1cmp 7118  geolim1i 7181  ele3lem 7276  ege2lem2 7278  ege2le3lem2 7279  efaddlem8 7295  efaddlem12 7299  efaddlem22 7309  sin01bndlem1 7417  ruclem25 7485  infmap2 7531  nmblolbii 8403  normlem6 8920  norm-ii 8943  projlem7 9131  nmbdoplb 9887

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409  df-op 2412  df-br 2615

Copyright terms: Public domain