Theorem ifeq12da

Description: Equivalence deduction for conditional operators. (Contributed by Wolf Lammen, 24-Jun-2021)

	Ref	Expression
Hypotheses	ifeq12da.1	$$⊢\left(\phi \wedge \psi \right)\to A=C$$
	ifeq12da.2	$$⊢\left(\phi \wedge \neg \psi \right)\to B=D$$
Assertion	ifeq12da	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\psi ,C,D\right)$$

Proof

Step	Hyp	Ref	Expression
1		ifeq12da.1	$$⊢\left(\phi \wedge \psi \right)\to A=C$$
2		ifeq12da.2	$$⊢\left(\phi \wedge \neg \psi \right)\to B=D$$
3	1	ifeq1da	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\psi ,C,B\right)$$
4		iftrue	$$⊢\psi \to if\left(\psi ,C,B\right)=C$$
5		iftrue	$$⊢\psi \to if\left(\psi ,C,D\right)=C$$
6	4 5	eqtr4d	$$⊢\psi \to if\left(\psi ,C,B\right)=if\left(\psi ,C,D\right)$$
7	3 6	sylan9eq	$$⊢\left(\phi \wedge \psi \right)\to if\left(\psi ,A,B\right)=if\left(\psi ,C,D\right)$$
8	2	ifeq2da	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\psi ,A,D\right)$$
9		iffalse	$$⊢\neg \psi \to if\left(\psi ,A,D\right)=D$$
10		iffalse	$$⊢\neg \psi \to if\left(\psi ,C,D\right)=D$$
11	9 10	eqtr4d	$$⊢\neg \psi \to if\left(\psi ,A,D\right)=if\left(\psi ,C,D\right)$$
12	8 11	sylan9eq	$$⊢\left(\phi \wedge \neg \psi \right)\to if\left(\psi ,A,B\right)=if\left(\psi ,C,D\right)$$
13	7 12	pm2.61dan	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\psi ,C,D\right)$$