Theorem ifex

Description: Existence of the conditional operator (inference form). (Contributed by NM, 2-Sep-2004)

	Ref	Expression
Hypotheses	ifex.1	$$⊢A\in \mathrm{V}$$
	ifex.2	$$⊢B\in \mathrm{V}$$
Assertion	ifex	$$⊢if\left(\phi ,A,B\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ifex.1	$$⊢A\in \mathrm{V}$$
2		ifex.2	$$⊢B\in \mathrm{V}$$
3	1 2	ifcli	$$⊢if\left(\phi ,A,B\right)\in \mathrm{V}$$