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 e. C
	ifcli.2	|- B e. C
Assertion	ifcli	|- if ( ph , A , B ) e. C

Proof

Step	Hyp	Ref	Expression
1		ifcli.1	|- A e. C
2		ifcli.2	|- B e. C
3		ifcl	|- ( ( A e. C /\ B e. C ) -> if ( ph , A , B ) e. C )
4	1 2 3	mp2an	|- if ( ph , A , B ) e. C