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	⊢ 𝐴 ∈ 𝐶
	ifcli.2	⊢ 𝐵 ∈ 𝐶
Assertion	ifcli	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) ∈ 𝐶

Proof

Step	Hyp	Ref	Expression
1		ifcli.1	⊢ 𝐴 ∈ 𝐶
2		ifcli.2	⊢ 𝐵 ∈ 𝐶
3		ifcl	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → if ( 𝜑 , 𝐴 , 𝐵 ) ∈ 𝐶 )
4	1 2 3	mp2an	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) ∈ 𝐶