Theorem 3brtr4d

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

	Ref	Expression
Hypotheses	3brtr4d.1	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
	3brtr4d.2	⊢ ( 𝜑 → 𝐶 = 𝐴 )
	3brtr4d.3	⊢ ( 𝜑 → 𝐷 = 𝐵 )
Assertion	3brtr4d	⊢ ( 𝜑 → 𝐶 𝑅 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		3brtr4d.1	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
2		3brtr4d.2	⊢ ( 𝜑 → 𝐶 = 𝐴 )
3		3brtr4d.3	⊢ ( 𝜑 → 𝐷 = 𝐵 )
4	2 3	breq12d	⊢ ( 𝜑 → ( 𝐶 𝑅 𝐷 ↔ 𝐴 𝑅 𝐵 ) )
5	1 4	mpbird	⊢ ( 𝜑 → 𝐶 𝑅 𝐷 )