Theorem ifeq12

Description: Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004)

	Ref	Expression
Assertion	ifeq12	$$⊢\left(A=B\wedge C=D\right)\to if\left(\phi ,A,C\right)=if\left(\phi ,B,D\right)$$

Proof

Step	Hyp	Ref	Expression
1		ifeq1	$$⊢A=B\to if\left(\phi ,A,C\right)=if\left(\phi ,B,C\right)$$
2		ifeq2	$$⊢C=D\to if\left(\phi ,B,C\right)=if\left(\phi ,B,D\right)$$
3	1 2	sylan9eq	$$⊢\left(A=B\wedge C=D\right)\to if\left(\phi ,A,C\right)=if\left(\phi ,B,D\right)$$