Theorem ifclda

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

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

Proof

Step	Hyp	Ref	Expression
1		ifclda.1	$$⊢\left(\phi \wedge \psi \right)\to A\in C$$
2		ifclda.2	$$⊢\left(\phi \wedge \neg \psi \right)\to B\in 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	eqeltrd	$$⊢\left(\phi \wedge \psi \right)\to if\left(\psi ,A,B\right)\in 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	eqeltrd	$$⊢\left(\phi \wedge \neg \psi \right)\to if\left(\psi ,A,B\right)\in C$$
9	5 8	pm2.61dan	$$⊢\phi \to if\left(\psi ,A,B\right)\in C$$