Theorem ifeq1da

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

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

Proof

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