Theorem iffalse

Description: Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999)

	Ref	Expression
Assertion	iffalse	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		dedlemb	$$⊢\neg \phi \to \left(x\in B\leftrightarrow \left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\right)$$
2	1	abbi2dv	$$⊢\neg \phi \to B=\left\{x|\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\right\}$$
3		df-if	$$⊢if\left(\phi ,A,B\right)=\left\{x|\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\right\}$$
4	2 3	syl6reqr	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$