Theorem breq12i

Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996) (Proof shortened by Eric Schmidt, 4-Apr-2007)

	Ref	Expression
Hypotheses	breq1i.1	$$⊢A=B$$
	breq12i.2	$$⊢C=D$$
Assertion	breq12i	$$⊢ARC\leftrightarrow BRD$$

Proof

Step	Hyp	Ref	Expression
1		breq1i.1	$$⊢A=B$$
2		breq12i.2	$$⊢C=D$$
3		breq12	$$⊢\left(A=B\wedge C=D\right)\to \left(ARC\leftrightarrow BRD\right)$$
4	1 2 3	mp2an	$$⊢ARC\leftrightarrow BRD$$