Theorem int-eqprincd

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

	Ref	Expression
Hypotheses	int-eqprincd.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	int-eqprincd.2	⊢ ( 𝜑 → 𝐶 = 𝐷 )
Assertion	int-eqprincd	⊢ ( 𝜑 → ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		int-eqprincd.1	⊢ ( 𝜑 → 𝐴 = 𝐵 )
2		int-eqprincd.2	⊢ ( 𝜑 → 𝐶 = 𝐷 )
3	1 2	oveq12d	⊢ ( 𝜑 → ( 𝐴 + 𝐶 ) = ( 𝐵 + 𝐷 ) )