Theorem ifexd

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

	Ref	Expression
Hypotheses	ifexd.1	|- ( ph -> A e. V )
	ifexd.2	|- ( ph -> B e. W )
Assertion	ifexd	|- ( ph -> if ( ps , A , B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		ifexd.1	|- ( ph -> A e. V )
2		ifexd.2	|- ( ph -> B e. W )
3	1	elexd	|- ( ph -> A e. _V )
4	2	elexd	|- ( ph -> B e. _V )
5	3 4	ifcld	|- ( ph -> if ( ps , A , B ) e. _V )