Theorem int-eqprincd

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

	Ref	Expression
Hypotheses	int-eqprincd.1	|- ( ph -> A = B )
	int-eqprincd.2	|- ( ph -> C = D )
Assertion	int-eqprincd	|- ( ph -> ( A + C ) = ( B + D ) )

Proof

Step	Hyp	Ref	Expression
1		int-eqprincd.1	|- ( ph -> A = B )
2		int-eqprincd.2	|- ( ph -> C = D )
3	1 2	oveq12d	|- ( ph -> ( A + C ) = ( B + D ) )