Theorem iftrue

Description: Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999) (Proof shortened by Andrew Salmon, 26-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		dfif2	$$⊢if\left(\phi ,A,B\right)=\left\{x|\left(\left(x\in B\to \phi \right)\to \left(x\in A\wedge \phi \right)\right)\right\}$$
2		dedlem0a	$$⊢\phi \to \left(x\in A\leftrightarrow \left(\left(x\in B\to \phi \right)\to \left(x\in A\wedge \phi \right)\right)\right)$$
3	2	eqabdv	$$⊢\phi \to A=\left\{x|\left(\left(x\in B\to \phi \right)\to \left(x\in A\wedge \phi \right)\right)\right\}$$
4	1 3	eqtr4id	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$