Theorem 3brtr4d

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005)

	Ref	Expression
Hypotheses	3brtr4d.1	$$⊢\phi \to ARB$$
	3brtr4d.2	$$⊢\phi \to C=A$$
	3brtr4d.3	$$⊢\phi \to D=B$$
Assertion	3brtr4d	$$⊢\phi \to CRD$$

Proof

Step	Hyp	Ref	Expression
1		3brtr4d.1	$$⊢\phi \to ARB$$
2		3brtr4d.2	$$⊢\phi \to C=A$$
3		3brtr4d.3	$$⊢\phi \to D=B$$
4	2 3	breq12d	$$⊢\phi \to \left(CRD\leftrightarrow ARB\right)$$
5	1 4	mpbird	$$⊢\phi \to CRD$$