Theorem ifeq2da

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

	Ref	Expression
Hypothesis	ifeq2da.1	|- ( ( ph /\ -. ps ) -> A = B )
Assertion	ifeq2da	|- ( ph -> if ( ps , C , A ) = if ( ps , C , B ) )

Proof

Step	Hyp	Ref	Expression
1		ifeq2da.1	|- ( ( ph /\ -. ps ) -> A = B )
2		iftrue	|- ( ps -> if ( ps , C , A ) = C )
3		iftrue	|- ( ps -> if ( ps , C , B ) = C )
4	2 3	eqtr4d	|- ( ps -> if ( ps , C , A ) = if ( ps , C , B ) )
5	4	adantl	|- ( ( ph /\ ps ) -> if ( ps , C , A ) = if ( ps , C , B ) )
6	1	ifeq2d	|- ( ( ph /\ -. ps ) -> if ( ps , C , A ) = if ( ps , C , B ) )
7	5 6	pm2.61dan	|- ( ph -> if ( ps , C , A ) = if ( ps , C , B ) )