Theorem ifeqda

Description: Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018)

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

Proof

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