Theorem ifcli

Description: Inference associated with ifcl . Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth when the special case B e. C is provable. (Contributed by NM, 14-Aug-1999) (Proof shortened by BJ, 1-Sep-2022)

	Ref	Expression
Hypotheses	ifcli.1	$$⊢A\in C$$
	ifcli.2	$$⊢B\in C$$
Assertion	ifcli	$$⊢if\left(\phi ,A,B\right)\in C$$

Proof

Step	Hyp	Ref	Expression
1		ifcli.1	$$⊢A\in C$$
2		ifcli.2	$$⊢B\in C$$
3		ifcl	$$⊢\left(A\in C\wedge B\in C\right)\to if\left(\phi ,A,B\right)\in C$$
4	1 2 3	mp2an	$$⊢if\left(\phi ,A,B\right)\in C$$