Theorem 3brtr4 2085

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

Syntax hints:   = wceq 1091   class class class wbr 2054

This theorem is referenced by:  cda1en 3721  cdacomen 3724  cdaassen 3725  xpcdaen 3726  1lt2pq 3872  0lt1sr 3998  nneo 4719  sqrlem2 4732  sqrlem11 4741  sqrlem16 4746  releabs 4858  abstri 4859  ruclem25 4909  normlem6 5068  norm-ii 5086  projlem5 5197  projlem7 5199

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-un 1490  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063

metamath.org