Theorem 3brtr4 2633

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 2624	. 2 |- CRB
4		3brtr4.3	. 2 |- D = B
5	3, 4	breqtrr 2630	1 |- CRD

Syntax hints:   = wceq 953   class class class wbr 2609

This theorem is referenced by:  1sdom2 4505  cda1en 4898  cdacomen 4901  cdaassen 4902  xpcdaen 4903  1lt2pq 5050  0lt1sr 5176  nneo 6144  sqrlem2 6604  sqrlem11 6613  sqrlem16 6618  abstri 6829  faclbnd4lem1 6885  ser1cmp 7110  geolim1i 7173  ele3lem 7268  ege2lem2 7270  ege2le3lem2 7271  efaddlem8 7287  efaddlem12 7291  efaddlem22 7301  sin01bndlem1 7409  ruclem25 7477  infmap2 7523  nmblolbii 8390  normlem6 8902  norm-ii 8925  projlem7 9108  nmbdoplb 9864

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610

Copyright terms: Public domain