Theorem ifexd

Description: Existence of the conditional operator (deduction form). (Contributed by SN, 26-Jul-2024)

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

Proof

Step	Hyp	Ref	Expression
1		ifexd.1	$$⊢\phi \to A\in V$$
2		ifexd.2	$$⊢\phi \to B\in W$$
3	1	elexd	$$⊢\phi \to A\in \mathrm{V}$$
4	2	elexd	$$⊢\phi \to B\in \mathrm{V}$$
5	3 4	ifcld	$$⊢\phi \to if\left(\psi ,A,B\right)\in \mathrm{V}$$