Theorem ifclda

Description: Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	ifclda.1	|- ( ( ph /\ ps ) -> A e. C )
	ifclda.2	|- ( ( ph /\ -. ps ) -> B e. C )
Assertion	ifclda	|- ( ph -> if ( ps , A , B ) e. C )

Proof

Step	Hyp	Ref	Expression
1		ifclda.1	|- ( ( ph /\ ps ) -> A e. C )
2		ifclda.2	|- ( ( ph /\ -. ps ) -> B e. C )
3		iftrue	|- ( ps -> if ( ps , A , B ) = A )
4	3	adantl	|- ( ( ph /\ ps ) -> if ( ps , A , B ) = A )
5	4 1	eqeltrd	|- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
6		iffalse	|- ( -. ps -> if ( ps , A , B ) = B )
7	6	adantl	|- ( ( ph /\ -. ps ) -> if ( ps , A , B ) = B )
8	7 2	eqeltrd	|- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
9	5 8	pm2.61dan	|- ( ph -> if ( ps , A , B ) e. C )