Theorem int-eqprincd

Description: PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

	Ref	Expression
Hypotheses	int-eqprincd.1	$$⊢\phi \to A=B$$
	int-eqprincd.2	$$⊢\phi \to C=D$$
Assertion	int-eqprincd	$$⊢\phi \to A+C=B+D$$

Proof

Step	Hyp	Ref	Expression
1		int-eqprincd.1	$$⊢\phi \to A=B$$
2		int-eqprincd.2	$$⊢\phi \to C=D$$
3	1 2	oveq12d	$$⊢\phi \to A+C=B+D$$