Theorem ifex

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

	Ref	Expression
Hypotheses	ifex.1	|- A e. _V
	ifex.2	|- B e. _V
Assertion	ifex	|- if ( ph , A , B ) e. _V

Proof

Step	Hyp	Ref	Expression
1		ifex.1	|- A e. _V
2		ifex.2	|- B e. _V
3	1 2	ifcli	|- if ( ph , A , B ) e. _V