Theorem ifeq3da

Description: Given an expression C containing if ( ps , E , F ) , substitute (hypotheses .1 and .2) and evaluate (hypotheses .3 and .4) it for both cases at the same time. (Contributed by Thierry Arnoux, 13-Dec-2021)

	Ref	Expression
Hypotheses	ifeq3da.1	$$⊢if\left(\psi ,E,F\right)=E\to C=G$$
	ifeq3da.2	$$⊢if\left(\psi ,E,F\right)=F\to C=H$$
	ifeq3da.3	$$⊢\phi \to G=A$$
	ifeq3da.4	$$⊢\phi \to H=B$$
Assertion	ifeq3da	$$⊢\phi \to if\left(\psi ,A,B\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		ifeq3da.1	$$⊢if\left(\psi ,E,F\right)=E\to C=G$$
2		ifeq3da.2	$$⊢if\left(\psi ,E,F\right)=F\to C=H$$
3		ifeq3da.3	$$⊢\phi \to G=A$$
4		ifeq3da.4	$$⊢\phi \to H=B$$
5		iftrue	$$⊢\psi \to if\left(\psi ,E,F\right)=E$$
6	5 1	syl	$$⊢\psi \to C=G$$
7	6	adantl	$$⊢\left(\phi \wedge \psi \right)\to C=G$$
8	3	adantr	$$⊢\left(\phi \wedge \psi \right)\to G=A$$
9	7 8	eqtr2d	$$⊢\left(\phi \wedge \psi \right)\to A=C$$
10		iffalse	$$⊢\neg \psi \to if\left(\psi ,E,F\right)=F$$
11	10 2	syl	$$⊢\neg \psi \to C=H$$
12	11	adantl	$$⊢\left(\phi \wedge \neg \psi \right)\to C=H$$
13	4	adantr	$$⊢\left(\phi \wedge \neg \psi \right)\to H=B$$
14	12 13	eqtr2d	$$⊢\left(\phi \wedge \neg \psi \right)\to B=C$$
15	9 14	ifeqda	$$⊢\phi \to if\left(\psi ,A,B\right)=C$$