Theorem ifeq2da

Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypothesis	ifeq2da.1	$$⊢\left(\phi \wedge \neg \psi \right)\to A=B$$
Assertion	ifeq2da	$$⊢\phi \to if\left(\psi ,C,A\right)=if\left(\psi ,C,B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ifeq2da.1	$$⊢\left(\phi \wedge \neg \psi \right)\to A=B$$
2		iftrue	$$⊢\psi \to if\left(\psi ,C,A\right)=C$$
3		iftrue	$$⊢\psi \to if\left(\psi ,C,B\right)=C$$
4	2 3	eqtr4d	$$⊢\psi \to if\left(\psi ,C,A\right)=if\left(\psi ,C,B\right)$$
5	4	adantl	$$⊢\left(\phi \wedge \psi \right)\to if\left(\psi ,C,A\right)=if\left(\psi ,C,B\right)$$
6	1	ifeq2d	$$⊢\left(\phi \wedge \neg \psi \right)\to if\left(\psi ,C,A\right)=if\left(\psi ,C,B\right)$$
7	5 6	pm2.61dan	$$⊢\phi \to if\left(\psi ,C,A\right)=if\left(\psi ,C,B\right)$$