Theorem 3brtr4d

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

	Ref	Expression
Hypotheses	3brtr4d.1	|- ( ph -> A R B )
	3brtr4d.2	|- ( ph -> C = A )
	3brtr4d.3	|- ( ph -> D = B )
Assertion	3brtr4d	|- ( ph -> C R D )

Proof

Step	Hyp	Ref	Expression
1		3brtr4d.1	|- ( ph -> A R B )
2		3brtr4d.2	|- ( ph -> C = A )
3		3brtr4d.3	|- ( ph -> D = B )
4	2 3	breq12d	|- ( ph -> ( C R D <-> A R B ) )
5	1 4	mpbird	|- ( ph -> C R D )